From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 6 Aug 2012 22:05:12 +0000 (+0000)
Subject: Support setting :regular-output-channel and :diagnostic-output-channel.
X-Git-Tag: cvc5-1.0.0~7884
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a99a3693b2c69ffd6a4268c9020593f62a3474eb;p=cvc5.git

Support setting :regular-output-channel and :diagnostic-output-channel.
Also some cleanup of option-related exceptions infrastructure.
---

diff --git a/configure.ac b/configure.ac
index 6820b2bb4..0e98152be 100644
--- a/configure.ac
+++ b/configure.ac
@@ -862,6 +862,9 @@ AC_CHECK_HEADERS([getopt.h unistd.h])
 
 AC_CHECK_DECLS([optreset], [], [], [#include <getopt.h>])
 
+# check with which standard strerror_r() complies
+AC_FUNC_STRERROR_R
+
 # require boost library
 BOOST_REQUIRE()
 
diff --git a/src/cvc4.i b/src/cvc4.i
index cddd3891c..08b2c509f 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -117,8 +117,10 @@ using namespace CVC4;
 %include "expr/expr_stream.i"
 
 %include "smt/smt_engine.i"
-%include "smt/bad_option_exception.i"
 %include "smt/no_such_function_exception.i"
 %include "smt/modal_exception.i"
 
+%include "options/options.i"
+%include "options/option_exception.i"
+
 %include "parser/cvc4parser.i"
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 576707fca..7f10c533e 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -25,7 +25,7 @@
 
 #include "expr/command.h"
 #include "smt/smt_engine.h"
-#include "smt/bad_option_exception.h"
+#include "options/options.h"
 #include "util/output.h"
 #include "util/dump.h"
 #include "util/sexpr.h"
@@ -963,7 +963,7 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
-  } catch(BadOptionException&) {
+  } catch(UnrecognizedOptionException&) {
     d_commandStatus = new CommandUnsupported();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -997,7 +997,7 @@ void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
        << response;
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
-  } catch(BadOptionException&) {
+  } catch(UnrecognizedOptionException&) {
     d_commandStatus = new CommandUnsupported();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -1047,7 +1047,7 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
-  } catch(BadOptionException&) {
+  } catch(UnrecognizedOptionException&) {
     d_commandStatus = new CommandUnsupported();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -1082,7 +1082,7 @@ void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
     ss << SExpr(v);
     d_result = ss.str();
     d_commandStatus = CommandSuccess::instance();
-  } catch(BadOptionException&) {
+  } catch(UnrecognizedOptionException&) {
     d_commandStatus = new CommandUnsupported();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
diff --git a/src/main/options b/src/main/options
index 6defc8642..47e397d11 100644
--- a/src/main/options
+++ b/src/main/options
@@ -30,8 +30,7 @@ option threadArgv std::vector<std::string>
 option thread_id int :default -1
  Thread ID, for internal use in case of multi-threaded run
 option separateOutput bool :default false
- In multi-threaded setting print output of each thread at the
- end of run, separated by a divider ("----").
+ In multi-threaded setting print output of each thread at the end of run, separated by a divider ("----").
 option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
  don't share lemmas strictly longer than N
 
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 2db54a4d9..e1cd721f3 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -28,7 +28,8 @@ noinst_LTLIBRARIES = liboptions.la
 
 liboptions_la_SOURCES = \
 	options.h \
-	base_options_handlers.h
+	base_options_handlers.h \
+	option_exception.h
 
 nodist_liboptions_la_SOURCES = \
 	options.cpp \
@@ -60,6 +61,7 @@ EXTRA_DIST = \
 	options_template.cpp \
 	options_holder_template.h \
 	options.i \
+	option_exception.i \
 	$(OPTIONS_FILES:%=../%)
 
 if CVC4_DEBUG
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 2bfd6a2d9..a551d5bd9 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -649,7 +649,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
         for handler in $handlers; do
           run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", value, smt);
+    $handler(\"$smtname\", optarg, smt);
 "
         done
       fi
@@ -665,7 +665,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
       for handler in $handlers; do
         run_handlers="$run_handlers
 #line $lineno \"$kf\"
-    $handler(\"$smtname\", value, smt);
+    $handler(\"$smtname\", optarg, smt);
 "
       done
       smt_setoption_handlers="${smt_setoption_handlers}
diff --git a/src/options/option_exception.h b/src/options/option_exception.h
new file mode 100644
index 000000000..657bc7568
--- /dev/null
+++ b/src/options/option_exception.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file option_exception.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: taking, cconway
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Options-related exceptions
+ **
+ ** Options-related exceptions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTION_EXCEPTION_H
+#define __CVC4__OPTION_EXCEPTION_H
+
+#include "util/exception.h"
+
+namespace CVC4 {
+
+/**
+ * Class representing an option-parsing exception such as badly-typed
+ * or missing arguments, arguments out of bounds, etc.  If an option
+ * name is itself unrecognized, a UnrecognizedOptionException (a derived
+ * class, below) should be used instead.
+ */
+class CVC4_PUBLIC OptionException : public CVC4::Exception {
+public:
+  OptionException(const std::string& s) throw() :
+    CVC4::Exception("Error in option parsing: " + s) {
+  }
+};/* class OptionException */
+
+/**
+ * Class representing an exception in option processing due to an
+ * unrecognized or unsupported option key.
+ */
+class CVC4_PUBLIC UnrecognizedOptionException : public CVC4::OptionException {
+public:
+  UnrecognizedOptionException() :
+    CVC4::OptionException("Unrecognized informational or option key or setting") {
+  }
+
+  UnrecognizedOptionException(const std::string& msg) :
+    CVC4::OptionException(msg) {
+  }
+};/* class UnrecognizedOptionException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTION_EXCEPTION_H */
diff --git a/src/options/option_exception.i b/src/options/option_exception.i
new file mode 100644
index 000000000..ae68d4e0f
--- /dev/null
+++ b/src/options/option_exception.i
@@ -0,0 +1,5 @@
+%{
+#include "options/option_exception.h"
+%}
+
+%include "options/option_exception.h"
diff --git a/src/options/options.h b/src/options/options.h
index a3abdd54b..c966670f5 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -25,7 +25,7 @@
 #include <fstream>
 #include <string>
 
-#include "util/exception.h"
+#include "options/option_exception.h"
 #include "util/language.h"
 #include "util/tls.h"
 
@@ -40,14 +40,6 @@ class NodeManager;
 class NodeManagerScope;
 class SmtEngine;
 
-/** Class representing an option-parsing exception. */
-class CVC4_PUBLIC OptionException : public CVC4::Exception {
-public:
-  OptionException(const std::string& s) throw() :
-    CVC4::Exception("Error in option parsing: " + s) {
-  }
-};/* class OptionException */
-
 class CVC4_PUBLIC Options {
   /** The struct that holds all option values. */
   options::OptionsHolder* d_holder;
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 9cc236a13..76cebbdd1 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -11,7 +11,6 @@ libsmt_la_SOURCES = \
 	smt_engine_scope.cpp \
 	smt_engine_scope.h \
 	modal_exception.h \
-	bad_option_exception.h \
 	no_such_function_exception.h \
 	simplification_mode.h \
 	simplification_mode.cpp
@@ -22,7 +21,6 @@ nodist_libsmt_la_SOURCES = \
 EXTRA_DIST = \
 	options_handlers.h \
 	smt_options_template.cpp \
-	bad_option_exception.i \
 	no_such_function_exception.i \
 	modal_exception.i \
 	smt_engine.i
diff --git a/src/smt/bad_option_exception.h b/src/smt/bad_option_exception.h
deleted file mode 100644
index 8fafb952e..000000000
--- a/src/smt/bad_option_exception.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*********************                                                        */
-/*! \file bad_option_exception.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief An exception that is thrown when an option setting is not
- ** understood.
- **
- ** An exception that is thrown when an interactive-only feature while
- ** CVC4 is being used in a non-interactive setting (for example, the
- ** "(get-assertions)" command in an SMT-LIBv2 script).
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__SMT__BAD_OPTION_EXCEPTION_H
-#define __CVC4__SMT__BAD_OPTION_EXCEPTION_H
-
-#include "util/exception.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC BadOptionException : public CVC4::Exception {
-public:
-  BadOptionException() :
-    Exception("Unrecognized informational or option key or setting") {
-  }
-
-  BadOptionException(const std::string& msg) :
-    Exception(msg) {
-  }
-
-  BadOptionException(const char* msg) :
-    Exception(msg) {
-  }
-};/* class BadOptionException */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__BAD_OPTION_EXCEPTION_H */
diff --git a/src/smt/bad_option_exception.i b/src/smt/bad_option_exception.i
deleted file mode 100644
index eeded5a45..000000000
--- a/src/smt/bad_option_exception.i
+++ /dev/null
@@ -1,7 +0,0 @@
-%{
-#include "smt/bad_option_exception.h"
-%}
-
-%ignore CVC4::BadOptionException::BadOptionException(const char*);
-
-%include "smt/bad_option_exception.h"
diff --git a/src/smt/options b/src/smt/options
index 5ee65e50a..13b3b51f3 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -55,6 +55,11 @@ option repeatSimp --repeat-simp bool :read-write
 common-option incrementalSolving incremental -i --incremental bool
  enable incremental solving
 
+option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h"
+ set the regular output channel of the solver
+option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
+ set the diagnostic output channel of the solver
+
 common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long"
  enable time limiting (give milliseconds)
 common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long"
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index f111f512b..925f86d48 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -21,11 +21,47 @@
 #ifndef __CVC4__SMT__OPTIONS_HANDLERS_H
 #define __CVC4__SMT__OPTIONS_HANDLERS_H
 
+#include "cvc4autoconfig.h"
 #include "util/dump.h"
 
+#include <cerrno>
+#include <cstring>
+#include <sstream>
+
 namespace CVC4 {
 namespace smt {
 
+static inline std::string __cvc4_errno_failreason() {
+#if HAVE_STRERROR_R
+#if STRERROR_R_CHAR_P
+  if(errno != 0) {
+    // GNU version of strerror_r: *might* use the given buffer,
+    // or might not.  It returns a pointer to buf, or not.
+    char buf[80];
+    return std::string(strerror_r(errno, buf, sizeof buf));
+  } else {
+    return "unknown reason";
+  }
+#else /* STRERROR_R_CHAR_P */
+  if(errno != 0) {
+    // XSI version of strerror_r: always uses the given buffer.
+    // Returns an error code.
+    char buf[80];
+    if(strerror_r(errno, buf, sizeof buf) == 0) {
+      return std::string(buf);
+    } else {
+      // some error occurred while getting the error string
+      return "unknown reason";
+    }
+  } else {
+    return "unknown reason";
+  }
+#endif /* STRERROR_R_CHAR_P */
+#else /* HAVE_STRERROR_R */
+  return "unknown reason";
+#endif /* HAVE_STRERROR_R */
+}
+
 static const std::string dumpHelp = "\
 Dump modes currently supported by the --dump option:\n\
 \n\
@@ -179,42 +215,107 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
 #endif /* CVC4_DUMPING */
 }
 
+inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "batch") {
+    return SIMPLIFICATION_MODE_BATCH;
+  } else if(optarg == "incremental") {
+    return SIMPLIFICATION_MODE_INCREMENTAL;
+  } else if(optarg == "none") {
+    return SIMPLIFICATION_MODE_NONE;
+  } else if(optarg == "help") {
+    puts(simplificationHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --simplification: `") +
+                          optarg + "'.  Try --simplification help.");
+  }
+}
+
+// This macro is used for setting :regular-output-channel and :diagnostic-output-channel
+// to redirect a stream.  It maintains all attributes set on the stream.
+#define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
+  { \
+    int dagSetting = expr::ExprDag::getDag(__channel_get); \
+    size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \
+    bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
+    OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \
+    __channel_set; \
+    __channel_get << Expr::dag(dagSetting); \
+    __channel_get << Expr::setdepth(exprDepthSetting); \
+    __channel_get << Expr::printtypes(printtypesSetting); \
+    __channel_get << Expr::setlanguage(languageSetting); \
+  }
+
 inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
 #ifdef CVC4_DUMPING
-  size_t dagSetting = expr::ExprDag::getDag(Dump.getStream());
+  std::ostream* outStream = NULL;
   if(optarg == "") {
     throw OptionException(std::string("Bad file name for --dump-to"));
   } else if(optarg == "-") {
-    Dump.setStream(DumpOutC::dump_cout);
+    outStream = &DumpOutC::dump_cout;
   } else {
-    std::ostream* dumpTo = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(!*dumpTo) {
-      throw OptionException(std::string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
+    errno = 0;
+    outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(outStream == NULL || !*outStream) {
+      std::stringstream ss;
+      ss << "Cannot open dump-to file: `" << optarg << "': " << __cvc4_errno_failreason();
+      throw OptionException(ss.str());
     }
-    Dump.setStream(*dumpTo);
   }
-  expr::ExprDag::setDag(Dump.getStream(), dagSetting);
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Dump.getStream(), Dump.setStream(*outStream));
 #else /* CVC4_DUMPING */
   throw OptionException("The dumping feature was disabled in this build of CVC4.");
 #endif /* CVC4_DUMPING */
 }
 
-inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "batch") {
-    return SIMPLIFICATION_MODE_BATCH;
-  } else if(optarg == "incremental") {
-    return SIMPLIFICATION_MODE_INCREMENTAL;
-  } else if(optarg == "none") {
-    return SIMPLIFICATION_MODE_NONE;
-  } else if(optarg == "help") {
-    puts(simplificationHelp.c_str());
-    exit(1);
+inline void setRegularOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
+  std::ostream* outStream = NULL;
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name setting for regular output channel"));
+  } else if(optarg == "stdout") {
+    outStream = &std::cout;
+  } else if(optarg == "stderr") {
+    outStream = &std::cerr;
   } else {
-    throw OptionException(std::string("unknown option for --simplification: `") +
-                          optarg + "'.  Try --simplification help.");
+    errno = 0;
+    outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(outStream == NULL || !*outStream) {
+      std::stringstream ss;
+      ss << "Cannot open regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
+      throw OptionException(ss.str());
+    }
+  }
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
+}
+
+inline void setDiagnosticOutputChannel(std::string option, std::string optarg, SmtEngine* smt) {
+  std::ostream* outStream = NULL;
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name setting for diagnostic output channel"));
+  } else if(optarg == "stdout") {
+    outStream = &std::cout;
+  } else if(optarg == "stderr") {
+    outStream = &std::cerr;
+  } else {
+    errno = 0;
+    outStream = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(outStream == NULL || !*outStream) {
+      std::stringstream ss;
+      ss << "Cannot open diagnostic-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
+      throw OptionException(ss.str());
+    }
   }
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Debug.getStream(), Debug.setStream(*outStream));
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Warning.getStream(), Warning.setStream(*outStream));
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Message.getStream(), Message.setStream(*outStream));
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Notice.getStream(), Notice.setStream(*outStream));
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Chat.getStream(), Chat.setStream(*outStream));
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(Trace.getStream(), Trace.setStream(*outStream));
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
 }
 
+#undef __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM
+
 inline std::string checkReplayFilename(std::string option, std::string optarg, SmtEngine* smt) {
 #ifdef CVC4_REPLAY
   if(optarg == "") {
@@ -234,9 +335,12 @@ inline std::ostream* checkReplayLogFilename(std::string option, std::string opta
   } else if(optarg == "-") {
     return &std::cout;
   } else {
+    errno = 0;
     std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(!*replayLog) {
-      throw OptionException(std::string("Cannot open replay-log file: `") + optarg + "'");
+    if(replayLog == NULL || !*replayLog) {
+      std::stringstream ss;
+      ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
+      throw OptionException(ss.str());
     }
     return replayLog;
   }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6b7ca8d2f..de5971306 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,7 +38,6 @@
 #include "expr/metakind.h"
 #include "expr/node_builder.h"
 #include "prop/prop_engine.h"
-#include "smt/bad_option_exception.h"
 #include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
 #include "smt/smt_engine.h"
@@ -50,6 +49,7 @@
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "smt/options.h"
+#include "options/option_exception.h"
 #include "util/output.h"
 #include "util/hash.h"
 #include "theory/substitutions.h"
@@ -607,7 +607,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
-  throw(BadOptionException, ModalException) {
+  throw(OptionException, ModalException) {
 
   SmtScope smts(this);
 
@@ -631,7 +631,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       string cvc4key = key.substr(6);
       if(cvc4key == "logic") {
         if(! value.isAtom()) {
-          throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string");
+          throw OptionException("argument to (set-info :cvc4-logic ..) must be a string");
         }
         SmtScope smts(this);
         d_logic = value.getValue();
@@ -656,17 +656,17 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
       s = value.getValue();
     }
     if(s != "sat" && s != "unsat" && s != "unknown") {
-      throw BadOptionException("argument to (set-info :status ..) must be "
-                               "`sat' or `unsat' or `unknown'");
+      throw OptionException("argument to (set-info :status ..) must be "
+                            "`sat' or `unsat' or `unknown'");
     }
     d_status = Result(s);
     return;
   }
-  throw BadOptionException();
+  throw UnrecognizedOptionException();
 }
 
 CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
-  throw(BadOptionException, ModalException) {
+  throw(OptionException, ModalException) {
 
   SmtScope smts(this);
 
@@ -721,7 +721,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
                            "last result wasn't unknown!");
     }
   } else {
-    throw BadOptionException();
+    throw UnrecognizedOptionException();
   }
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 52a2e0c27..505a2d8d8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -30,7 +30,6 @@
 #include "expr/expr_manager.h"
 #include "util/proof.h"
 #include "util/model.h"
-#include "smt/bad_option_exception.h"
 #include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
 #include "util/hash.h"
@@ -303,25 +302,25 @@ public:
    * Set information about the script executing.
    */
   void setInfo(const std::string& key, const CVC4::SExpr& value)
-    throw(BadOptionException, ModalException);
+    throw(OptionException, ModalException);
 
   /**
    * Query information about the SMT environment.
    */
   CVC4::SExpr getInfo(const std::string& key) const
-    throw(BadOptionException, ModalException);
+    throw(OptionException, ModalException);
 
   /**
    * Set an aspect of the current SMT execution environment.
    */
   void setOption(const std::string& key, const CVC4::SExpr& value)
-    throw(BadOptionException, ModalException);
+    throw(OptionException, ModalException);
 
   /**
    * Get an aspect of the current SMT execution environment.
    */
   CVC4::SExpr getOption(const std::string& key) const
-    throw(BadOptionException);
+    throw(OptionException);
 
   /**
    * Add a formula to the current context: preprocess, do per-theory
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
index f34a0e2db..b254a3b30 100644
--- a/src/smt/smt_options_template.cpp
+++ b/src/smt/smt_options_template.cpp
@@ -17,7 +17,6 @@
  **/
 
 #include "smt/smt_engine.h"
-#include "smt/bad_option_exception.h"
 #include "smt/modal_exception.h"
 #include "util/sexpr.h"
 #include "util/dump.h"
@@ -30,14 +29,14 @@
 ${include_all_option_headers}
 ${option_handler_includes}
 
-#line 34 "${template}"
+#line 33 "${template}"
 
 using namespace std;
 
 namespace CVC4 {
 
 void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
-  throw(BadOptionException, ModalException) {
+  throw(OptionException, ModalException) {
 
   NodeManagerScope nms(d_nodeManager);
   SmtEngine* const smt = this;
@@ -51,13 +50,13 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
 
   ${smt_setoption_handlers}
 
-#line 55 "${template}"
+#line 54 "${template}"
 
-  throw BadOptionException();
+  throw UnrecognizedOptionException();
 }
 
 CVC4::SExpr SmtEngine::getOption(const std::string& key) const
-  throw(BadOptionException) {
+  throw(OptionException) {
 
   NodeManagerScope nms(d_nodeManager);
 
@@ -68,9 +67,9 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 
   ${smt_getoption_handlers}
 
-#line 72 "${template}"
+#line 71 "${template}"
 
-  throw BadOptionException();
+  throw UnrecognizedOptionException();
 }
 
 }/* CVC4 namespace */