Support setting :regular-output-channel and :diagnostic-output-channel.

Also some cleanup of option-related exceptions infrastructure.

5 files changed, 69 insertions, 12 deletions

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;