Options merge. This commit:

1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)

The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:

* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important.  If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***

Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).

Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double).  For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).

Benefits of the new options system include:

1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose

I've taken lots of care not to break anything.  Hopefully, I've succeeded in that.

11 files changed, 2444 insertions, 0 deletions

diff --git a/src/options/Makefile b/src/options/Makefile
new file mode 100644
index 000000000..54a46191d
--- /dev/null
+++ b/src/options/Makefile
@@ -0,0 +1,4 @@
+topdir = ../..
+srcdir = src/options
+
+include $(topdir)/Makefile.subdir
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
new file mode 100644
index 000000000..1f4e991a5
--- /dev/null
+++ b/src/options/Makefile.am
@@ -0,0 +1,134 @@
+OPTIONS_FILES = \
+	options/base_options \
+	expr/options \
+	theory/booleans/options \
+	theory/options \
+	theory/bv/options \
+	theory/datatypes/options \
+	theory/builtin/options \
+	theory/arith/options \
+	theory/uf/options \
+	theory/arrays/options \
+	theory/quantifiers/options \
+	theory/rewriterules/options \
+	prop/options \
+	proof/options \
+	printer/options \
+	smt/options \
+	decision/options \
+	main/options \
+	parser/options
+
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
+AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = liboptions.la
+
+liboptions_la_SOURCES = \
+	options.h \
+	base_options_handlers.h
+
+nodist_liboptions_la_SOURCES = \
+	options.cpp \
+	options_holder.h \
+	$(OPTIONS_FILES:%=../%.cpp) \
+	$(OPTIONS_FILES:%=../%.h)
+nodist_liboptions_la_OBJECTS = \
+	$(patsubst %.cpp,%.lo,$(filter %.cpp,$(nodist_liboptions_la_SOURCES)))
+
+BUILT_SOURCES = \
+	options.cpp \
+	options_holder.h \
+	base_options.cpp \
+	base_options.h \
+	../smt/smt_options.cpp \
+	$(OPTIONS_FILES:%=../%.cpp) \
+	$(OPTIONS_FILES:%=../%.h) \
+	exprs-builts
+
+DISTCLEANFILES = \
+	$(BUILT_SOURCES) \
+	options-stamp
+
+EXTRA_DIST = \
+	mkoptions \
+	base_options \
+	base_options_template.h \
+	base_options_template.cpp \
+	options_template.cpp \
+	options_holder_template.h \
+	options.i \
+	$(OPTIONS_FILES:%=../%)
+
+if CVC4_DEBUG
+# listing Debug_tags too ensures that make doesn't auto-remove it
+# after building (if it does, we don't get the "cached" effect with
+# the .tmp files below, and we have to re-compile and re-link each
+# time, even when there are no changes).
+BUILT_SOURCES += \
+	Debug_tags.h \
+	Debug_tags
+endif
+if CVC4_TRACING
+# listing Trace_tags too ensures that make doesn't auto-remove it
+# after building (if it does, we don't get the "cached" effect with
+# the .tmp files below, and we have to re-compile and re-link each
+# time, even when there are no changes).
+BUILT_SOURCES += \
+	Trace_tags.h \
+	Trace_tags
+endif
+%_tags.h: %_tags
+	$(AM_V_GEN)( \
+	  echo 'static char const* const $^[] = {'; \
+	  for tag in `cat $^`; do \
+	    echo "\"$$tag\","; \
+	  done; \
+	  echo 'NULL'; \
+	  echo '};' \
+	) >"$@"
+
+# This .tmp business is to keep from having to re-compile options.cpp
+# (and then re-link the libraries) if nothing has changed.
+%_tags: %_tags.tmp
+	$(AM_V_GEN)\
+	diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true
+# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
+.PHONY: Debug_tags.tmp Trace_tags.tmp
+# The "sed" invocation below is particularly obnoxious, but it works around
+# inconsistencies in REs on different platforms, using only a basic regular
+# expression (no |, no \<, ...).
+Debug_tags.tmp Trace_tags.tmp:
+	$(AM_V_GEN)\
+	grep '\<$(@:_tags.tmp=) *( *\".*\" *)' \
+		`find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
+	sed 's/^$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/' | sort | uniq >"$@"
+
+MOSTLYCLEANFILES = \
+	Debug_tags \
+	Trace_tags \
+	Debug_tags.tmp \
+	Trace_tags.tmp \
+	Debug_tags.h \
+	Trace_tags.h
+
+options_holder.h options.cpp ../smt/smt_options.cpp base_options.cpp base_options.h $(OPTIONS_FILES:%=../%.cpp) $(OPTIONS_FILES:%=../%.h): options-stamp
+options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILES:%=../%)
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions \
+		@srcdir@/options_holder_template.h @srcdir@/options_holder.h \
+		@srcdir@/options_template.cpp @srcdir@/options.cpp \
+		@srcdir@/../smt/smt_options_template.cpp @srcdir@/../smt/smt_options.cpp \
+		@top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \
+		-t \
+		@srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \
+		$(foreach o,$(OPTIONS_FILES),"$(srcdir)/../$(o)" "$(dir $(srcdir)/../$(o))") \
+	)
+	touch "$@"
+
+base_options $(OPTIONS_FILES:%=../%):;
+
+.PHONY: exprs-builts
+exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true
diff --git a/src/options/base_options b/src/options/base_options
new file mode 100644
index 000000000..10ad564e6
--- /dev/null
+++ b/src/options/base_options
@@ -0,0 +1,110 @@
+#
+# Option specification file for CVC4
+#
+# This is essentially a shell script interpreted with special commands.
+#
+# Lines starting with whitespace are special.  They are passed in their entirety (minus
+# the first whitespace char) to the "doc" command.  Lines starting with a single slash
+# are stripped of this initial character and interpreted by the "doc-alt" command.  A period
+# "." in the first column of a line, followed optionally by whitespace but without any other
+# content on the line, is interpreted as an empty string passed to doc.  (This allows
+# multi-paragraph documentation for options.)  Lines may be continued with a backslash (\)
+# at the end of a line.
+#
+# commands are:
+#
+#   module ID "include-file" name
+#
+#     Identifies the module.  Must be the first command in the file.  ID is a suitable
+#     identifier for a preprocessor definition, and should be unique; name is a "pretty"
+#     name used for the benefit of the end CVC4 user in, e.g., option listings.
+#
+#   common-option SPECIFICATION
+#   option SPECIFICATION
+#   expert-option SPECIFICATION
+#   undocumented-option SPECIFICATION
+#
+#     These commands declare (respectively) common options presented first to the user,
+#     standard options that the user might want to see with "--help" documentation,
+#     expert options that should be marked as expert-only, and options that should not
+#     appear in normal option documentation (even if documentation is included here).
+#
+#     SPECIFICATIONs take this form:
+#
+#       SPECIFICATION ::= (internal-name | -) [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] [smt-option-name] C++-type [ATTRIBUTEs...]
+#       ATTRIBUTE ::=   :include include-files..
+#                     | :default C++-expression
+#                     | :handler custom-option-handlers..
+#                     | :handler-include include-files..
+#                     | :read-only
+#                     | :read-write
+#                     | :link linked-options..
+#
+#   alias smt-option-name = (smt-option-name[=argument])+
+#   alias (-short-option | --long-option) = (-option[=argument] | --long-option[=argument])+
+#
+#     The alias command creates a new SmtEngine option name, or short option, or long option,
+#     and binds it to act the same way as if the options to the right of "=" were passed.
+#     For example, if there are options to --disable-warning-1 and --disable-warning-2, etc.,
+#     a useful alias might be:
+#
+#       alias --disable-all-warnings = --disable-warning-1 --disable-warning-2
+#
+#     Aliases cannot take arguments, and command-line aliases cannot set SmtEngine properties,
+#     and SmtEngine aliases cannot set command-line properties.  For these things, you need a
+#     custom handler.
+#
+#   warning message
+#
+#     Warn about something during processing (like a FIXME).
+#
+#   endmodule
+#
+#     This file should end with the "endmodule" command, and nothing should follow it.
+#
+
+module BASE "options/base_options.h" Base
+
+option binary_name std::string
+
+option in std::istream* :default &std::cin :include <iostream>
+option out std::ostream* :default &std::cout :include <iostream>
+option err std::ostream* :default &std::cerr :include <iostream>
+
+common-option inputLanguage -L --lang=LANG InputLanguage :handler CVC4::options::stringToInputLanguage :include "util/language.h" :default language::input::LANG_AUTO :read-write
+ force input language (default is "auto"; see --lang help)
+common-option outputLanguage --output-lang=LANG OutputLanguage :handler CVC4::options::stringToOutputLanguage :include "util/language.h" :default language::output::LANG_AUTO :read-write
+ force input language (default is "auto"; see --lang help)
+option languageHelp bool
+
+option verbosity verbosity int :read-write :default 0
+ the verbosity level of CVC4
+common-option - -v --verbose void :handler CVC4::options::increaseVerbosity
+ increase verbosity (may be repeated)
+common-option - -q --quiet void :handler CVC4::options::decreaseVerbosity
+ decrease verbosity (may be repeated)
+
+common-option statistics stats --stats bool
+ give statistics on exit
+
+common-option parseOnly parse-only --parse-only bool :read-write
+ exit after parsing input
+
+common-option preprocessOnly preprocess-only --preprocess-only bool
+ exit after preprocessing input
+
+option segvNoSpin --segv-nospin bool
+ don't spin on segfault waiting for gdb
+
+option - -t --trace=TAG argument :handler CVC4::options::addTraceTag
+ trace something (e.g. -t pushpop), can repeat
+option - -d --debug=TAG argument :handler CVC4::options::addDebugTag
+ debug something (e.g. -d arith), can repeat
+
+option printSuccess print-success --print-success bool :predicate CVC4::options::setPrintSuccess :predicate-include "options/base_options_handlers.h"
+ print the "success" output required of SMT-LIBv2
+
+alias --smtlib2 = --lang=smt2 --output-lang=smt2 --strict-parsing --default-expr-depth=-1 --print-success
+ SMT-LIBv2 compliance mode (implies other options)
+
+endmodule
diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h
new file mode 100644
index 000000000..5f82280da
--- /dev/null
+++ b/src/options/base_options_handlers.h
@@ -0,0 +1,173 @@
+/*********************                                                        */
+/*! \file base_options_handlers.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-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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#ifndef __CVC4__BASE_OPTIONS_HANDLERS_H
+#define __CVC4__BASE_OPTIONS_HANDLERS_H
+
+#include <iostream>
+#include <string>
+#include <sstream>
+
+#include "expr/command.h"
+
+namespace CVC4 {
+namespace options {
+
+inline void increaseVerbosity(std::string option, SmtEngine* smt) {
+  options::verbosity.set(options::verbosity() + 1);
+}
+
+inline void decreaseVerbosity(std::string option, SmtEngine* smt) {
+  options::verbosity.set(options::verbosity() - 1);
+}
+
+inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "cvc4" || optarg == "pl") {
+    return language::output::LANG_CVC4;
+  } else if(optarg == "smtlib" || optarg == "smt") {
+    return language::output::LANG_SMTLIB;
+  } else if(optarg == "smtlib2" || optarg == "smt2") {
+    return language::output::LANG_SMTLIB_V2;
+  } else if(optarg == "tptp") {
+    return language::output::LANG_TPTP;
+  } else if(optarg == "ast") {
+    return language::output::LANG_AST;
+  } else if(optarg == "auto") {
+    return language::output::LANG_AUTO;
+  }
+
+  if(optarg != "help") {
+    throw OptionException(std::string("unknown language for --output-lang: `") +
+                          optarg + "'.  Try --output-lang help.");
+  }
+
+  options::languageHelp.set(true);
+  return language::output::LANG_AUTO;
+}
+
+inline InputLanguage stringToInputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "cvc4" || optarg == "pl" || optarg == "presentation") {
+    return language::input::LANG_CVC4;
+  } else if(optarg == "smtlib" || optarg == "smt") {
+    return language::input::LANG_SMTLIB;
+  } else if(optarg == "smtlib2" || optarg == "smt2") {
+    return language::input::LANG_SMTLIB_V2;
+  } else if(optarg == "tptp") {
+    return language::input::LANG_TPTP;
+  } else if(optarg == "auto") {
+    return language::input::LANG_AUTO;
+  }
+
+  if(optarg != "help") {
+    throw OptionException(std::string("unknown language for --lang: `") +
+                          optarg + "'.  Try --lang help.");
+  }
+
+  options::languageHelp.set(true);
+  return language::input::LANG_AUTO;
+}
+
+inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) {
+  if(Configuration::isTracingBuild()) {
+    if(!Configuration::isTraceTag(optarg.c_str()))
+      throw OptionException(std::string("trace tag ") + optarg +
+                            std::string(" not available"));
+  } else {
+    throw OptionException("trace tags not available in non-tracing builds");
+  }
+  Trace.on(optarg);
+}
+
+inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt) {
+  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
+    if(!Configuration::isDebugTag(optarg.c_str()) &&
+       !Configuration::isTraceTag(optarg.c_str())) {
+      throw OptionException(std::string("debug tag ") + optarg +
+                            std::string(" not available"));
+    }
+  } else if(! Configuration::isDebugBuild()) {
+    throw OptionException("debug tags not available in non-debug builds");
+  } else {
+    throw OptionException("debug tags not available in non-tracing builds");
+  }
+  Debug.on(optarg);
+  Trace.on(optarg);
+}
+
+inline void setPrintSuccess(std::string option, bool value, SmtEngine* smt) {
+  Debug.getStream() << Command::printsuccess(value);
+  Trace.getStream() << Command::printsuccess(value);
+  Notice.getStream() << Command::printsuccess(value);
+  Chat.getStream() << Command::printsuccess(value);
+  Message.getStream() << Command::printsuccess(value);
+  Warning.getStream() << Command::printsuccess(value);
+  *options::out() << Command::printsuccess(value);
+}
+
+template <template <class U> class Cmp>
+class comparator {
+  long d_lbound;
+  double d_dbound;
+  bool d_hasLbound;
+
+public:
+  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) {}
+
+  template <class T>
+  void operator()(std::string option, const T& value, SmtEngine* smt) {
+    if((d_hasLbound && !(Cmp<T>()(value, T(d_lbound)))) ||
+       (!d_hasLbound && !(Cmp<T>()(value, T(d_dbound))))) {
+      std::stringstream ss;
+      ss << option << ": " << value << " is not a legal setting";
+      throw OptionException(ss.str());
+    }
+  }
+};/* class comparator */
+
+struct greater : public comparator<std::greater> {
+  greater(long l) throw() : comparator<std::greater>(l) {}
+  greater(double d) throw() : comparator<std::greater>(d) {}
+};/* struct greater */
+
+struct greater_equal : public comparator<std::greater_equal> {
+  greater_equal(long l) throw() : comparator<std::greater_equal>(l) {}
+  greater_equal(double d) throw() : comparator<std::greater_equal>(d) {}
+};/* struct greater_equal */
+
+struct less : public comparator<std::less> {
+  less(long l) throw() : comparator<std::less>(l) {}
+  less(double d) throw() : comparator<std::less>(d) {}
+};/* struct less */
+
+struct less_equal : public comparator<std::less_equal> {
+  less_equal(long l) throw() : comparator<std::less_equal>(l) {}
+  less_equal(double d) throw() : comparator<std::less_equal>(d) {}
+};/* struct less_equal */
+
+struct not_equal : public comparator<std::not_equal_to> {
+  not_equal(long l) throw() : comparator<std::not_equal_to>(l) {}
+  not_equal(double d) throw() : comparator<std::not_equal_to>(d) {}
+};/* struct not_equal_to */
+
+}/* CVC4::options namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__BASE_OPTIONS_HANDLERS_H */
+
diff --git a/src/options/base_options_template.cpp b/src/options/base_options_template.cpp
new file mode 100644
index 000000000..97d747652
--- /dev/null
+++ b/src/options/base_options_template.cpp
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file base_options_template.cpp
+ ** \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 Contains code for handling command-line options.
+ **
+ ** Contains code for handling command-line options
+ **/
+
+#include "options/options_holder.h"
+
+namespace CVC4 {
+
+${module_accessors}
+
+#line 26 "${template}"
+
+namespace options {
+
+${module_global_definitions}
+
+#line 32 "${template}"
+
+}/* CVC4::options namespace */
+
+}/* CVC4 namespace */
diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h
new file mode 100644
index 000000000..211cb866a
--- /dev/null
+++ b/src/options/base_options_template.h
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file base_options_template.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 Contains code for handling command-line options.
+ **
+ ** Contains code for handling command-line options
+ **/
+
+#ifndef __CVC4__OPTIONS__${module_id}_H
+#define __CVC4__OPTIONS__${module_id}_H
+
+#include "options/options.h"
+${module_includes}
+
+#line 26 "${template}"
+
+${module_optionholder_spec}
+
+#line 30 "${template}"
+
+namespace CVC4 {
+
+namespace options {
+
+${module_decls}
+
+#line 38 "${template}"
+
+}/* CVC4::options namespace */
+
+${module_specializations}
+
+#line 44 "${template}"
+
+namespace options {
+
+${module_inlines}
+
+#line 50 "${template}"
+
+}/* CVC4::options namespace */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTIONS__${module_id}_H */
diff --git a/src/options/mkoptions b/src/options/mkoptions
new file mode 100755
index 000000000..2bfd6a2d9
--- /dev/null
+++ b/src/options/mkoptions
@@ -0,0 +1,1260 @@
+#!/bin/bash
+#
+# mkoptions
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2011  The CVC4 Project
+#
+# The purpose of this script is to create options.{h,cpp}
+# from template files and a list of options.
+#
+# Invocation:
+#
+#   mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+
+#
+
+copyright=2011
+
+me=$(basename "$0")
+
+function usage {
+  echo "usage: $me (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+" >&2
+}
+
+declare -a templates
+declare -a outputs
+
+while [ "$1" != -t ]; do
+  if [ "$#" -lt 2 ]; then
+    echo "$me: error: expected -t on command line" >&2
+    usage
+    exit 1
+  fi
+  templates[${#templates[@]}]="$1"; shift
+  if [ "$1" = -t ]; then
+    echo "$me: error: mismatched number of templates and output files (before -t)" >&2
+    usage
+    exit 1
+  fi
+  outputs[${#outputs[@]}]="$1"; shift
+done
+
+shift
+if [ "$#" -lt 3 ]; then
+  echo "$me: error: not enough arguments" >&2
+  usage
+  exit 1
+fi
+
+options_h_template="$1"; shift
+options_cpp_template="$1"; shift
+
+all_modules_defaults=
+all_modules_short_options=
+all_modules_long_options=
+all_modules_option_handlers=
+smt_getoption_handlers=
+smt_setoption_handlers=
+include_all_option_headers=
+all_modules_contributions=
+option_handler_includes=
+all_custom_handlers=
+common_documentation=
+remaining_documentation=
+common_manpage_documentation=
+remaining_manpage_documentation=
+
+seen_module=false
+seen_endmodule=false
+expect_doc=false
+expect_doc_alternate=false
+n_long=256
+
+internal=
+smtname=
+short_option=
+short_option_alternate=
+long_option=
+long_option_alternate=
+long_option_alternate_set=
+type=
+predicates=
+
+# just for duplicates-checking
+all_declared_internal_options=
+all_declared_long_options=
+all_declared_short_options=
+all_declared_smt_options=
+
+long_option_value_begin=$n_long
+
+function module {
+  # module id name
+
+  module_id=
+  module_name=
+  module_includes=
+  module_optionholder_spec=
+  module_decls=
+  module_specializations=
+  module_inlines=
+  module_accessors=
+  module_global_definitions=
+
+  seen_module=true
+  if [ $# -lt 3 -o -z "$1" -o -z "$2" -o -z "$3" ]; then
+    echo "$kf:$lineno: error: \"module\" directive requires exactly three arguments" >&2
+    exit 1
+  fi
+
+  module_id="$1"; shift
+  include="$1"; shift
+  module_name="$@"
+  include_all_option_headers="${include_all_option_headers}
+#line $lineno \"$kf\"
+#include $(check_include "$include")"
+  all_modules_contributions="${all_modules_contributions}
+  CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
+  module_optionholder_spec="#define CVC4_OPTIONS__${module_id}__FOR_OPTION_HOLDER"
+
+  remaining_documentation="${remaining_documentation}\\n\\n\"
+#line $lineno \"$kf\"
+\"$module_name options:"
+  remaining_manpage_documentation="${remaining_manpage_documentation}
+.SH `echo "$module_name" | tr a-z A-Z` OPTIONS
+"
+}
+
+function endmodule {
+  # endmodule
+  check_module_seen
+  check_doc
+  seen_endmodule=true
+  if [ $# -ne 0 ]; then
+    echo "$kf:$lineno: error: endmodule takes no arguments" >&2
+    exit 1
+  fi
+}
+
+function common-option {
+  # common-option option-args...
+  handle_option COMMON "$@"
+}
+
+function option {
+  # option option-args...
+  handle_option STANDARD "$@"
+}
+
+function expert-option {
+  # expert-option option-args...
+  handle_option EXPERT "$@"
+}
+
+function undocumented-option {
+  # undocumented-option option-args...
+  handle_option UNDOCUMENTED "$@"
+}
+
+function handle_option {
+  check_module_seen
+  check_doc
+
+  args=("$@")
+
+  category="${args[0]}"
+  internal="${args[1]}"
+  smtname=
+  short_option=
+  short_option_alternate=
+  long_option=
+  long_option_alternate=
+  long_option_alternate_set=
+  type=
+  readOnly=true
+  required_argument=false
+  default_value=
+  handlers=
+  predicates=
+  links=
+  links_alternate=
+
+  options_already_documented=false
+  alternate_options_already_documented=false
+
+  if [ "$category" = UNDOCUMENTED ]; then
+    expect_doc=false
+  else
+    expect_doc=true
+  fi
+  expect_doc_alternate=false
+
+  # scan ahead to see where the type is
+  type_pos=2
+  while [ $(($type_pos+1)) -lt ${#args[@]} ] && ! expr "${args[$(($type_pos+1))]}" : ":" &>/dev/null; do
+    let ++type_pos
+  done
+
+  type="${args[$type_pos]}"
+
+  if [ "$type" = argument ]; then
+    type=void
+    required_argument=true
+  fi
+
+  if [ $type_pos -eq 2 ]; then
+    expect_doc=false
+    readOnly=false
+  else
+    i=2
+    while [ $i -lt $type_pos ]; do
+      if expr "${args[$i]}" : '--' &>/dev/null || expr "${args[$i]}" : '/--' &>/dev/null; then
+        if [ -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
+          exit 1
+        fi
+        long_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
+        if [ -n "$long_option" ]; then
+          if ! expr "$long_option" : '--.' &>/dev/null; then
+            echo "$kf:$option: bad long option \`$long_option': expected something like \`--foo'" >&2
+            exit 1
+          fi
+          long_option="$(echo "$long_option" | sed 's,^--,,')"
+        fi
+        if expr "${args[$i]}" : '.*/' &>/dev/null; then
+          long_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
+          long_option_alternate_set=set
+          if [ -n "$long_option_alternate" ]; then
+            if ! expr "$long_option_alternate" : '--.' &>/dev/null; then
+              echo "$kf:$option: bad alternate long option \`$long_option_alternate': expected something like \`--foo'" >&2
+              exit 1
+            fi
+            long_option_alternate="$(echo "$long_option_alternate" | sed 's,^--,,')"
+          fi
+        fi
+      elif expr "${args[$i]}" : '-' &>/dev/null || expr "${args[$i]}" : '/-' &>/dev/null; then
+        if [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
+          exit 1
+        fi
+        short_option="$(echo "${args[$i]}" | sed 's,/.*,,')"
+        if [ -n "$short_option" ]; then
+          if ! expr "$short_option" : '-.$' &>/dev/null; then
+            echo "$kf:$option: bad short option \`$short_option': expected something like \`-x'" >&2
+            exit 1
+          fi
+          short_option="$(echo "$short_option" | sed 's,^-,,')"
+        fi
+        if expr "${args[$i]}" : '.*/' &>/dev/null; then
+          short_option_alternate="$(echo "${args[$i]}" | sed 's,[^/]*/,,')"
+          if expr "$short_option_alternate" : - &>/dev/null; then
+            if ! expr "$short_option_alternate" : '-.$' &>/dev/null; then
+              echo "$kf:$option: bad alternate short option \`$short_option_alternate': expected something like \`-x'" >&2
+              exit 1
+            fi
+            short_option_alternate="$(echo "$short_option_alternate" | sed 's,^-,,')"
+          fi
+        fi
+      else
+        if [ -n "$smtname" -o -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o -n "$long_option_alternate" ]; then
+          echo "$kf:$lineno: error: malformed option line for \`$internal': unexpected \`${args[$i]}'" >&2
+          exit 1
+        fi
+        smtname="${args[$i]}"
+      fi
+      let ++i
+    done
+  fi
+
+  if [ "$type" = void -a "$internal" != - ]; then
+    echo "$kf:$lineno: error: $internal cannot be void-typed; use \`-' as the name if its to be void" >&2
+    exit 1
+  elif [ "$type" != void -a "$internal" = - ]; then
+    echo "$kf:$lineno: error: cannot use an unnamed option if its type is not void" >&2
+    exit 1
+  fi
+
+  if [ "$type" = bool -a -n "$long_option$short_option" -a "$category" != UNDOCUMENTED ]; then
+    if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then
+      expect_doc_alternate=true
+    fi
+  fi
+  if [ "$type" = bool -a -n "$long_option" -a -z "$long_option_alternate" -a -z "$long_option_alternate_set" ]; then
+    long_option_alternate="no-$(echo "$long_option" | sed 's,^--,,')"
+  fi
+  if [ "$type" != bool -a -n "$short_option_alternate" ]; then
+    echo "$kf:$lineno: error: cannot use alternate short option -$short_option_alternate for \`$internal' because it's not of bool type" >&2
+    exit 1
+  elif [ "$type" != bool -a -n "$long_option_alternate" ]; then
+    echo "$kf:$lineno: error: cannot use alternate long option --$long_option_alternate for \`$internal' because it's not of bool type" >&2
+    exit 1
+  fi
+
+  # check for duplicates
+  if [ "$internal" != - ]; then
+    if echo " $all_declared_internal_options " | grep -q " $internal "; then
+      echo "$kf:$lineno: error: internal option name \`$internal' previously declared" >&2
+      exit 1
+    fi
+    all_declared_internal_options="$all_declared_internal_options $internal"
+  fi
+  if [ -n "$long_option" ]; then
+    if echo " $all_declared_long_options " | grep -q " $long_option "; then
+      echo "$kf:$lineno: error: long option name \`--$long_option' previously declared" >&2
+      exit 1
+    fi
+    all_declared_long_options="$all_declared_long_options $long_option"
+  fi
+  if [ -n "$long_option_alternate" ]; then
+    if echo " $all_declared_long_options " | grep -q " $long_option_alternate "; then
+      echo "$kf:$lineno: error: long option name \`--$long_option_alternate' previously declared" >&2
+      exit 1
+    fi
+    all_declared_long_options="$all_declared_long_options $long_option_alternate"
+  fi
+  if [ -n "$short_option" ]; then
+    if echo " $all_declared_short_options " | grep -q " $short_option "; then
+      echo "$kf:$lineno: error: short option name \`-$short_option' previously declared" >&2
+      exit 1
+    fi
+    all_declared_short_options="$all_declared_short_options $short_option"
+  fi
+  if [ -n "$short_option_alternate" ]; then
+    if echo " $all_declared_short_options " | grep -q " $short_option_alternate "; then
+      echo "$kf:$lineno: error: short option name \`-$short_option_alternate' previously declared" >&2
+      exit 1
+    fi
+    all_declared_short_options="$all_declared_short_options $short_option_alternate"
+  fi
+  if [ -n "$smtname" ]; then
+    if echo " $all_declared_smt_options " | grep -q " $smtname "; then
+      echo "$kf:$lineno: error: SMT option name \`$smtname' previously declared" >&2
+      exit 1
+    fi
+    all_declared_smt_options="$all_declared_smt_options $smtname"
+  fi
+
+  # parse attributes
+  i=$(($type_pos+1))
+  while [ $i -lt ${#args[@]} ]; do
+    attribute="${args[$i]}"
+    case "$attribute" in
+    :default)
+       let ++i
+       default_value="${args[$i]}"
+       ;;
+    :handler)
+       let ++i
+       if [ -n "$handlers" ]; then
+         echo "$kf:$lineno: error: cannot specify more than one handler; maybe you want a :handler and a :predicate" >&2
+         exit 1
+       fi
+       handlers="${args[$i]}"
+       ;;
+    :predicate)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         predicates="${predicates} ${args[$i]}"
+       done
+       ;;
+    :link)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         link="${args[$i]}"
+         if expr "${args[$i]}" : '.*/' &>/dev/null; then
+           links="${links} $(echo "${args[$i]}" | sed 's,/.*,,')"
+           links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')"
+         else
+           links="${links} ${args[$i]}"
+           links_alternate="${links_alternate} ${args[$i]}"
+         fi
+       done
+       ;;
+    :include)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         module_includes="${module_includes}
+#line $lineno \"$kf\"
+#include $(check_include "${args[$i]}")"
+       done
+       ;;
+    :handler-include|:predicate-include)
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : ":" &>/dev/null; do
+         let ++i
+         option_handler_includes="${option_handler_includes}
+#line $lineno \"$kf\"
+#include $(check_include "${args[$i]}")"
+       done
+       ;;
+    :read-write)
+       readOnly=false
+       ;;
+    :read-only)
+       readOnly=true
+       ;;
+    *)
+       echo "$kf:$lineno: error in option \`$internal': bad attribute \`$attribute'" >&2
+       exit 1
+    esac
+    let ++i
+  done
+
+  # set up structures
+  if [ "$internal" != - ]; then
+    # set up a field in the options_holder
+    module_optionholder_spec="${module_optionholder_spec} \\
+  ${internal}__option_t::type $internal; \\
+  bool ${internal}__setByUser__;"
+    all_modules_defaults="${all_modules_defaults:+${all_modules_defaults},}
+#line $lineno \"$kf\"
+  $internal($default_value),
+#line $lineno \"$kf\"
+  ${internal}__setByUser__(false)"
+    if $readOnly; then
+      module_decls="${module_decls}
+#line $lineno \"$kf\"
+extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; } $internal CVC4_PUBLIC;"
+      module_inlines="${module_inlines}
+#line $lineno \"$kf\"
+inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
+#line $lineno \"$kf\"
+inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
+"
+    else
+      module_decls="${module_decls}
+#line $lineno \"$kf\"
+extern struct CVC4_PUBLIC ${internal}__option_t { typedef $type type; type operator()() const; bool wasSetByUser() const; void set(const type& v); } $internal CVC4_PUBLIC;"
+      module_inlines="${module_inlines}
+#line $lineno \"$kf\"
+inline ${internal}__option_t::type ${internal}__option_t::operator()() const { return Options::current()[*this]; }
+#line $lineno \"$kf\"
+inline bool ${internal}__option_t::wasSetByUser() const { return Options::current().wasSetByUser(*this); }
+#line $lineno \"$kf\"
+inline void ${internal}__option_t::set(const ${internal}__option_t::type& v) { Options::current().set(*this, v); }
+"
+      module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x);"
+      module_accessors="${module_accessors}
+#line $lineno \"$kf\"
+template <> void Options::set(options::${internal}__option_t, const options::${internal}__option_t::type& x) { d_holder->$internal = x; }"
+    fi
+    module_global_definitions="${module_global_definitions}
+#line $lineno \"$kf\"
+struct ${internal}__option_t $internal;"
+    module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const;
+#line $lineno \"$kf\"
+template <> bool Options::wasSetByUser(options::${internal}__option_t) const;"
+    if [ "$type" = bool ]; then
+      module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt);"
+    elif [ "$internal" != - ]; then
+      module_specializations="${module_specializations}
+#line $lineno \"$kf\"
+template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt);"
+    fi
+
+    module_accessors="${module_accessors}
+#line $lineno \"$kf\"
+template <> const options::${internal}__option_t::type& Options::operator[](options::${internal}__option_t) const { return d_holder->$internal; }
+#line $lineno \"$kf\"
+template <> bool Options::wasSetByUser(options::${internal}__option_t) const { return d_holder->${internal}__setByUser__; }"
+  fi
+
+  if $required_argument || [ "$type" != bool -a "$type" != void ]; then
+    expect_arg=:
+    expect_arg_long=required_argument
+  else
+    expect_arg=
+    expect_arg_long=no_argument
+  fi
+  cases=
+  cases_alternate=
+  if [ -n "$short_option" ]; then
+    all_modules_short_options="${all_modules_short_options}$short_option$expect_arg"
+    cases="${cases}
+    case '$short_option':"
+  fi
+  if [ -n "$short_option_alternate" ]; then
+    all_modules_short_options="${all_modules_short_options}$short_option_alternate$expect_arg"
+    cases_alternate="${cases_alternate}
+    case '$short_option_alternate':"
+  fi
+  if [ -n "$long_option" ]; then
+    all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$long_option" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
+    cases="${cases}
+    case $n_long:// --$long_option"
+    let ++n_long
+  fi
+  if [ -n "$long_option_alternate" ]; then
+    all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$long_option_alternate" | sed 's,=.*,,')\", $expect_arg_long, NULL, $n_long },"
+    cases_alternate="${cases_alternate}
+    case $n_long:// --$long_option_alternate"
+    let ++n_long
+  fi
+  run_links=
+  run_links_alternate=
+  if [ -n "$links" ]; then
+    for link in $links; do
+      run_links="$run_links
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, \"$link\");"
+    done
+  fi
+  if [ -n "$links_alternate" ]; then
+    for link in $links_alternate; do
+      run_links_alternate="$run_links_alternate
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, \"$link\");"
+    done
+  fi
+  if [ "$type" = bool -a -n "$cases" -o -n "$cases_alternate" ]; then
+    run_handlers=
+    if [ -n "$handlers" ]; then
+      echo "$kf:$lineno: error: bool-valued options cannot have handlers" >&2
+      exit 1
+    fi
+    if [ -n "$predicates" ]; then
+      for predicate in $predicates; do
+        run_handlers="$run_handlers
+#line $lineno \"$kf\"
+  $predicate(option, b, smt);"
+      done
+    fi
+    if [ -n "$run_handlers" ]; then
+      all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> void runBoolPredicates(options::${internal}__option_t, std::string option, bool b, SmtEngine* smt) {
+  $run_handlers
+}"
+    fi
+  fi
+  if [ -n "$cases" ]; then
+    if [ "$type" = bool ]; then
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], true, NULL);$run_links
+      break;
+"
+    elif [ -n "$expect_arg" -a "$internal" != - ]; then
+      run_handlers=
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+  $handler(option, optarg, smt);"
+        done
+      else
+        run_handlers="
+#line $lineno \"$kf\"
+  handleOption<$type>(option, optarg);"
+      fi
+      if [ -n "$predicates" ]; then
+        for predicate in $predicates; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+  $predicate(option, retval, smt);"
+        done
+      fi
+      all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> options::${internal}__option_t::type runHandlerAndPredicates(options::${internal}__option_t, std::string option, std::string optarg, SmtEngine* smt) {
+#line $lineno \"$kf\"
+  options::${internal}__option_t::type retval = $run_handlers
+#line $lineno \"$kf\"
+  return retval;
+}"
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      assign(options::$internal, argv[old_optind == 0 ? 1 : old_optind], optarg, NULL);$run_links
+      break;
+"
+    elif [ -n "$expect_arg" ]; then
+      run_handlers=
+      if [ -n "$predicates" ]; then
+        echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
+        exit 1
+      fi
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+      $handler(argv[old_optind == 0 ? 1 : old_optind], optarg, smt);"
+        done
+      fi
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      $run_handlers$run_links
+      break;
+"
+    else
+      run_handlers=
+      if [ -n "$predicates" ]; then
+        echo "$kf:$lineno: error: void-valued options cannot have predicates" >&2
+        exit 1
+      fi
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+      $handler(argv[old_optind == 0 ? 1 : old_optind], smt);"
+        done
+      fi
+      all_modules_option_handlers="${all_modules_option_handlers}${cases}
+#line $lineno \"$kf\"
+      $run_handlers$run_links
+      break;
+"
+    fi
+  fi
+  if [ -n "$cases_alternate" ]; then
+    if [ "$type" = bool ]; then
+      all_modules_option_handlers="${all_modules_option_handlers}${cases_alternate}
+#line $lineno \"$kf\"
+      assignBool(options::$internal, argv[old_optind == 0 ? 1 : old_optind], false, NULL);$run_links_alternate
+      break;
+"
+    else
+      echo "$kf:$lineno: internal error: expected BOOL-typed option in alternate handler" >&2
+      exit 1
+    fi
+  fi
+
+  if [ -n "$smtname" ]; then
+    if [ "$internal" != - ]; then
+      smt_getoption_handlers="${smt_getoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    stringstream ss; ss << options::$internal();
+    return SExpr(ss.str());
+  }"
+    fi
+
+    if [ "$type" = bool ]; then
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    Options::current().assignBool(options::$internal, \"$smtname\", optarg == \"true\", smt);$run_links
+    return;
+  }"
+    elif [ -n "$expect_arg" -a "$internal" != - ]; then
+      run_handlers=
+      if [ -n "$handlers" ]; then
+        for handler in $handlers; do
+          run_handlers="$run_handlers
+#line $lineno \"$kf\"
+    $handler(\"$smtname\", value, smt);
+"
+        done
+      fi
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    Options::current().assign(options::$internal, \"$smtname\", optarg, smt);$run_links
+    return;
+  }"
+    elif [ -n "$expect_arg" ]; then
+      run_handlers=
+      for handler in $handlers; do
+        run_handlers="$run_handlers
+#line $lineno \"$kf\"
+    $handler(\"$smtname\", value, smt);
+"
+      done
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    $run_handlers$run_links
+    return;
+  }"
+    else
+      run_handlers=
+      for handler in $handlers; do
+        run_handlers="$run_handlers
+#line $lineno \"$kf\"
+    $handler(\"$smtname\", smt);
+"
+      done
+      smt_setoption_handlers="${smt_setoption_handlers}
+#line $lineno \"$kf\"
+  if(key == \"$smtname\") {
+#line $lineno \"$kf\"
+    $run_handlers$run_links
+    return;
+  }"
+    fi
+  fi
+
+  if [ "$type" = bool ]; then
+    # emit assignBool/assign
+    all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> void Options::assignBool(options::${internal}__option_t, std::string option, bool value, SmtEngine* smt) {
+#line $lineno \"$kf\"
+  runBoolPredicates(options::$internal, option, value, smt);
+#line $lineno \"$kf\"
+  d_holder->$internal = value;
+#line $lineno \"$kf\"
+  d_holder->${internal}__setByUser__ = true;
+#line $lineno \"$kf\"
+  Trace(\"options\") << \"user assigned option $internal\" << std::endl;
+}"
+  elif [ -n "$expect_arg" -a "$internal" != - ] && [ -n "$cases" -o "$cases_alternate" -o "$smtname" ]; then
+    all_custom_handlers="${all_custom_handlers}
+#line $lineno \"$kf\"
+template <> void Options::assign(options::${internal}__option_t, std::string option, std::string value, SmtEngine* smt) {
+#line $lineno \"$kf\"
+  d_holder->$internal = runHandlerAndPredicates(options::$internal, option, value, smt);
+#line $lineno \"$kf\"
+  d_holder->${internal}__setByUser__ = true;
+#line $lineno \"$kf\"
+  Trace(\"options\") << \"user assigned option $internal\" << std::endl;
+}"
+  fi
+}
+
+function alias {
+  # alias (smtname | -option) = (smtname [arg] | -option [arg])+
+  check_module_seen
+  check_doc
+
+  category=STANDARD
+  internal=-
+  smtname=
+  short_option=
+  short_option_alternate=
+  long_option=
+  long_option_alternate=
+  long_option_alternate_set=
+  type=void
+  readOnly=true
+  required_argument=false
+  default_value=
+  handlers=
+  predicates=
+  links=
+  links_alternate=
+
+  options_already_documented=false
+  alternate_options_already_documented=false
+
+  if [ $# -lt 3 ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
+    exit 1
+  fi
+  options=
+  while [ $# -gt 0 -a "$1" != = ]; do
+    options="$options $1"
+    shift
+  done
+  if [ $# -eq 0 ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected \`='" >&2
+    exit 1
+  fi
+  shift
+  if [ $# -eq 0 ]; then
+    echo "$kf:$lineno: error: malformed \"alias\" command; expected more arguments" >&2
+    exit 1
+  fi
+  cases=
+  for option in $options; do
+    if ! expr "$option" : - &>/dev/null; then
+      echo "$kf:$lineno: error: alias for SMT options not yet supported" >&2
+      exit 1
+    fi
+    if expr "$option" : -- &>/dev/null; then
+      option="$(echo "$option" | sed 's,--,,')"
+      all_modules_long_options="${all_modules_long_options}
+  { \"$(echo "$option" | sed 's,=.*,,')\", no_argument, NULL, $n_long },"
+      cases="${cases}
+    case $n_long:// --$option"
+      let ++n_long
+      long_option="${long_option:+$long_option | --}$option"
+    else
+      if ! expr "$option" : '-.$' &>/dev/null; then
+        echo "$kf:$lineno: error: expected short option specification, got \`$option'" >&2
+        exit 1
+      fi
+      option="$(echo "$option" | sed 's,-,,')"
+      all_modules_short_options="${all_modules_short_options}$option"
+      cases="${cases}
+    case '$option':"
+      short_option="${short_option:+$short_option | -}$option"
+    fi
+  done
+  while [ $# -gt 0 ]; do
+    links="$links
+#line $lineno \"$kf\"
+      preemptGetopt(extra_argc, extra_argv, \"$1\");"
+    shift
+  done
+  all_modules_option_handlers="$all_modules_option_handlers$cases$links
+      break;
+"
+  expect_doc=true
+  expect_doc_alternate=false
+}
+
+function warning {
+  # warning message
+  check_module_seen
+  check_doc
+
+  echo "$kf:$lineno: warning: $@" >&2
+}
+
+function doc {
+  # doc text...
+  check_module_seen
+  expect_doc=false
+
+  if [ -z "$short_option" -a -z "$long_option" ]; then
+    if [ -n "$short_option_alternate" -o -n "$long_option_alternate" ]; then
+      if [ -n "$smtname" ]; then
+        expect_doc_alternate=true
+      else
+        doc-alternate "$@"
+        return
+      fi
+    fi
+  fi
+
+  if [ "$category" = UNDOCUMENTED ]; then
+    return
+  fi
+
+  if ! $options_already_documented; then
+    options_already_documented=true
+    the_opt=
+    if [ "$long_option" ]; then
+      the_opt="--$long_option"
+      if [ "$short_option" ]; then
+        shortoptarg=
+        if expr "$the_opt" : '.*=' &>/dev/null; then
+          shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
+        fi
+        the_opt="$the_opt | -$short_option$shortoptarg"
+      fi
+    elif [ "$short_option" ]; then
+      the_opt="-$short_option"
+    fi
+    if [ -z "$the_opt" ]; then
+      # nothing to document
+      return
+    fi
+
+    the_doc="$@"
+    if [ "$category" = EXPERT ]; then
+      the_doc="$the_doc (EXPERTS only)"
+    fi
+
+    doc_line=
+    while [ -n "$the_doc" ]; do
+      remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
+      the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
+      if [ -z "$doc_line" ]; then
+        if expr "$the_opt" : '.\{23\}' &>/dev/null; then
+          # break into two lines
+          doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
+        else
+          doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
+        fi
+      else
+        doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
+      fi
+      the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
+    done
+
+    if [ "$category" = COMMON ]; then
+      common_documentation="${common_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      common_manpage_documentation="${common_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    else
+      remaining_documentation="${remaining_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    fi
+  else
+    if [ "$category" = COMMON ]; then
+      common_manpage_documentation="${common_manpage_documentation}
+$@"
+    else
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+$@"
+    fi
+  fi
+}
+
+function doc-alternate {
+  # doc-alternate text...
+  check_module_seen
+  expect_doc_alternate=false
+
+  if $expect_doc; then
+    echo "$kf:$lineno: error: must provide documentation before alternate documentation" >&2
+    exit 1
+  fi
+
+  if [ -z "$short_option_alternate" -a -z "$long_option_alternate" ]; then
+    echo "$kf:$lineno: cannot document an alternative for option \`$internal'; one does not exist" >&2
+    exit 1
+  fi
+
+  if [ "$category" = UNDOCUMENTED ]; then
+    return
+  fi
+
+  if ! $alternate_options_already_documented; then
+    alternate_options_already_documented=true
+    the_opt=
+    if [ "$long_option_alternate" ]; then
+      the_opt="--$long_option_alternate"
+      shortoptarg=
+      if expr "$the_opt" : '.*=' &>/dev/null; then
+        shortoptarg="$(echo "$the_opt" | sed 's,[^=]*=, ,')"
+      fi
+      if [ "$short_option_alternate" ]; then
+        the_opt="$the_opt | -$short_option_alternate$shortoptarg"
+      fi
+    elif [ "$short_option_alternate" ]; then
+      the_opt="-$short_option_alternate"
+    fi
+    if [ -z "$the_opt" ]; then
+      # nothing to document
+      return
+    fi
+
+    the_doc="$@"
+    if [ "$category" = EXPERT ]; then
+      the_doc="$the_doc (EXPERTS only)"
+    fi
+
+    doc_line=
+    while [ -n "$the_doc" ]; do
+      remaining_doc="$(expr "$the_doc " : '.\{1,53\} \(.*\)')"
+      the_doc="$(expr "$the_doc " : '\(.\{1,53\}\) ')"
+      if [ -z "$doc_line" ]; then
+        if expr "$the_opt" : '.\{23\}' &>/dev/null; then
+          # break into two lines
+          doc_line="$(printf '  %s\\n\\\n%-24s %s' "$the_opt" "" "$the_doc")"
+        else
+          doc_line="$(printf '  %-22s %s' "$the_opt" "$the_doc")"
+        fi
+      else
+        doc_line="$doc_line\\n$(printf '%-24s %s' "" "$the_doc")"
+      fi
+      the_doc="$(expr "$remaining_doc" : '\(.*\) ')"
+    done
+
+    if [ "$category" = COMMON ]; then
+      common_documentation="${common_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      common_manpage_documentation="${common_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    else
+      remaining_documentation="${remaining_documentation}\\n\"
+#line $lineno \"$kf\"
+\"$(echo "$doc_line" | sed 's,'\'',\\'\'',g;s,",\\",g')"
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+.IP \"$the_opt\"
+$@"
+    fi
+  else
+    if [ "$category" = COMMON ]; then
+      common_manpage_documentation="${common_manpage_documentation}
+$@"
+    else
+      remaining_manpage_documentation="${remaining_manpage_documentation}
+$@"
+    fi
+  fi
+}
+
+function check_doc {
+  if $expect_doc; then
+    if [ "$internal" != - ]; then
+      echo "$kf:$lineno: warning: $internal is lacking documentation" >&2
+    elif [ -n "$long_option" ]; then
+      echo "$kf:$lineno: warning: option --$long_option is lacking documentation" >&2
+    elif [ -n "$short_option" ]; then
+      echo "$kf:$lineno: warning: option -$short_option is lacking documentation" >&2
+    elif [ -n "$smtname" ]; then
+      echo "$kf:$lineno: warning: SMT option $smtname is lacking documentation" >&2
+    fi
+    expect_doc=false
+  fi
+
+  if $expect_doc_alternate; then
+    echo "$kf:$lineno: warning: $internal is lacking documentation for the alternative option(s): $short_option_alternate $long_option_alternate" >&2
+    expect_doc_alternate=false
+  fi
+}
+
+function check_module_seen {
+  if $seen_endmodule; then
+    echo "$kf:$lineno: error: command after \"endmodule\" declaration (endmodule has to be last)" >&2
+    exit 1
+  fi
+  if ! $seen_module; then
+    echo "$kf:$lineno: error: no \"module\" declaration found (it has to be first)" >&2
+    exit 1
+  fi
+}
+
+function check_include {
+  if ! expr "$1" : '".*"$' &>/dev/null && ! expr "$1" : '<.*>$' &>/dev/null; then
+    echo "\"$1\""
+  else
+    echo "$1"
+  fi
+}
+
+function output_module {
+  template="$1"
+  output="$2"
+
+  filename="$(basename "$output")"
+
+  #echo "generating module $output from $template"
+
+  # generate warnings about incorrect #line annotations in templates
+  nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
+    awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+
+  text=$(cat "$template")
+  for var in \
+      module_id \
+      module_name \
+      module_includes \
+      module_optionholder_spec \
+      module_decls \
+      module_specializations \
+      module_inlines \
+      module_accessors \
+      module_global_definitions \
+      template \
+      ; do
+    eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+  done
+  error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)"
+  if [ -n "$error" ]; then
+    error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
+    echo "$template:0: error: undefined replacement \${$error}" >&2
+    exit 1
+  fi
+
+  (
+
+  # Output header (if this is a .cpp or .c or .h file) and then the
+  # processed text
+
+  if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then
+
+  cat <<EOF
+/*********************                                                        */
+/** $filename
+ **
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ **
+ ** This file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* Edit the template file instead:                     */
+/* $1 */
+
+EOF
+  fi
+
+  echo "$text"
+
+  ) >"$output.tmp"
+
+  diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output")
+  rm -f "$output.tmp"
+}
+
+while [ $# -gt 0 ]; do
+  kf="$1"; shift
+  if [ $# -eq 0 ]; then
+    echo "$me: error: mismatched number of templates and output files (before -t)" >&2
+    usage
+    exit 1
+  fi
+  outdir="$1"; shift
+
+  #echo "scanning $kf"
+
+  seen_module=false
+  seen_endmodule=false
+  b=$(basename $(dirname "$kf"))
+  lineno=0
+  # IFS= forces read to read an entire line
+  while IFS= read -r line; do
+    let ++lineno
+    # read any continuations of the line
+    while expr "$line" : '.*\\$' &>/dev/null; do
+      IFS= read -r line2
+      line="$(echo "$line" | sed 's,\\$,,')$line2"
+      let ++lineno
+    done
+    if expr "$line" : '[ 	].*' &>/dev/null; then
+      doc "$(echo "$line" | sed 's,^[ 	],,')"
+    elif expr "$line" : '\.[ 	]*$' &>/dev/null; then
+      doc ""
+    elif expr "$line" : '\.' &>/dev/null; then
+      echo "$kf:$lineno: error: malformed line during processing of option \`$internal': continuation lines should not have content" >&2
+      exit 1
+    elif expr "$line" : '/.*' &>/dev/null; then
+      doc-alternate "$(echo "$line" | sed 's,^/,,')"
+    else
+      line="$(echo "$line" | sed 's,\([<>&()!?*]\),\\\1,g')"
+      if ! eval "$line"; then
+        echo "$kf:$lineno: error was due to evaluation of this line" >&2
+        exit 1
+      fi
+    fi
+  done < "$kf"
+  if ! $seen_module; then
+    echo "$kf: error: no module content found in file!" >&2
+    exit 1
+  fi
+  if ! $seen_endmodule; then
+    echo "$kf:$lineno: error: no \"endmodule\" declaration found (it is required at the end)" >&2
+    exit 1
+  fi
+
+  output_module "$options_h_template" "$outdir/$(basename "$kf").h"
+  output_module "$options_cpp_template" "$outdir/$(basename "$kf").cpp"
+done
+
+## final outputs
+
+i=0; while [ $i -lt ${#templates[@]} ]; do
+
+template="${templates[$i]}"
+output="${outputs[$i]}"
+
+let ++i
+
+filename="$(basename "$output")"
+
+#echo "generating $output from $template"
+
+# generate warnings about incorrect #line annotations in templates
+nl -ba -s' ' "$template"  | grep '^ *[0-9][0-9]* # *line' |
+  awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2
+
+long_option_value_end=$n_long
+
+text=$(cat "$template")
+for var in \
+    all_modules_defaults \
+    all_modules_short_options \
+    all_modules_long_options \
+    all_modules_option_handlers \
+    include_all_option_headers \
+    all_modules_contributions \
+    option_handler_includes \
+    all_custom_handlers \
+    common_documentation \
+    remaining_documentation \
+    common_manpage_documentation \
+    remaining_manpage_documentation \
+    smt_getoption_handlers \
+    smt_setoption_handlers \
+    long_option_value_begin \
+    long_option_value_end \
+    template \
+    ; do
+  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error="$(echo "$text" | grep '.*\${[^}]*}.*' | head -n 1)"
+if [ -n "$error" ]; then
+  error="$(echo "$error" | sed 's,.*\${\([^}]*\)}.*,\1,')"
+  echo "$template:0: error: undefined replacement \${$error}" >&2
+  exit 1
+fi
+
+(
+
+# Output header (if this is a .cpp or .c or .h file) and then the
+# processed text
+
+if expr "$output" : '.*\.cpp$' &>/dev/null || expr "$output" : '.*\.[ch]$' &>/dev/null; then
+
+cat <<EOF
+/*********************                                                        */
+/** $filename
+ **
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ **
+ ** This file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
+
+/* Edit the template file instead:                     */
+/* $1 */
+
+EOF
+fi
+
+echo "$text"
+
+) >"$output.tmp"
+
+diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output")
+rm -f "$output.tmp"
+
+done
+
diff --git a/src/options/options.h b/src/options/options.h
new file mode 100644
index 000000000..a3abdd54b
--- /dev/null
+++ b/src/options/options.h
@@ -0,0 +1,150 @@
+/*********************                                                        */
+/*! \file options.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, 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 Global (command-line, set-option, ...) parameters for SMT.
+ **
+ ** Global (command-line, set-option, ...) parameters for SMT.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__OPTIONS__OPTIONS_H
+#define __CVC4__OPTIONS__OPTIONS_H
+
+#include <iostream>
+#include <fstream>
+#include <string>
+
+#include "util/exception.h"
+#include "util/language.h"
+#include "util/tls.h"
+
+namespace CVC4 {
+
+namespace options {
+  class OptionsHolder;
+}/* CVC4::options namespace */
+
+class ExprStream;
+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;
+
+  /** The current Options in effect */
+  static CVC4_THREADLOCAL(Options*) s_current;
+
+  /** Low-level assignment function for options */
+  template <class T>
+  void assign(T, std::string option, std::string value, SmtEngine* smt);
+  /** Low-level assignment function for bool-valued options */
+  template <class T>
+  void assignBool(T, std::string option, bool value, SmtEngine* smt);
+
+  friend class NodeManager;
+  friend class NodeManagerScope;
+  friend class SmtEngine;
+
+public:
+
+  /** Get the current Options in effect */
+  static inline Options& current() {
+    return *s_current;
+  }
+
+  Options();
+  Options(const Options& options);
+  ~Options();
+
+  /**
+   * Set the value of the given option.  Use of this default
+   * implementation causes a compile-time error; write-able
+   * options specialize this template with a real implementation.
+   */
+  template <class T>
+  void set(T, const typename T::type&) {
+    // Flag a compile-time error.  Write-able options specialize
+    // this template to provide an implementation.
+    T::you_are_trying_to_assign_to_a_read_only_option;
+  }
+
+  /** Get the value of the given option.  Const access only. */
+  template <class T>
+  const typename T::type& operator[](T) const;
+
+  /**
+   * Returns true iff the value of the given option was set
+   * by the user via a command-line option or SmtEngine::setOption().
+   * (Options::set() is low-level and doesn't count.)  Returns false
+   * otherwise.
+   */
+  template <class T>
+  bool wasSetByUser(T) const;
+
+  /**
+   * Get a description of the command-line flags accepted by
+   * parseOptions.  The returned string will be escaped so that it is
+   * suitable as an argument to printf. */
+  std::string getDescription() const;
+
+  /**
+   * Print overall command-line option usage message, prefixed by
+   * "msg"---which could be an error message causing the usage
+   * output in the first place, e.g. "no such option --foo"
+   */
+  static void printUsage(const std::string msg, std::ostream& out);
+
+  /**
+   * Print command-line option usage message for only the most-commonly
+   * used options.  The message is prefixed by "msg"---which could be
+   * an error message causing the usage output in the first place, e.g.
+   * "no such option --foo"
+   */
+  static void printShortUsage(const std::string msg, std::ostream& out);
+
+  /** Print help for the --lang command line option */
+  static void printLanguageHelp(std::ostream& out);
+
+  /**
+   * Initialize the options based on the given command-line arguments.
+   */
+  int parseOptions(int argc, char* argv[]) throw(OptionException);
+
+  /**
+   * Set the output language based on the given string.
+   */
+  void setOutputLanguage(const char* str) throw(OptionException);
+
+  /**
+   * Set the input language based on the given string.
+   */
+  void setInputLanguage(const char* str) throw(OptionException);
+
+};/* class Options */
+
+}/* CVC4 namespace */
+
+#include "options/base_options.h"
+
+#endif /* __CVC4__OPTIONS__OPTIONS_H */
diff --git a/src/options/options.i b/src/options/options.i
new file mode 100644
index 000000000..25eecaf2d
--- /dev/null
+++ b/src/options/options.i
@@ -0,0 +1,10 @@
+%{
+#include "options/options.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, SimplificationMode);
+%ignore CVC4::operator<<(std::ostream&, ArithPivotRule);
+
+%apply char** STRING_ARRAY { char* argv[] }
+%include "options/options.h"
+%clear char* argv[];
diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h
new file mode 100644
index 000000000..5b2c9a35d
--- /dev/null
+++ b/src/options/options_holder_template.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file options_holder_template.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 Global (command-line, set-option, ...) parameters for SMT
+ **
+ ** Global (command-line, set-option, ...) parameters for SMT.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__OPTIONS__OPTIONS_HOLDER_H
+#define __CVC4__OPTIONS__OPTIONS_HOLDER_H
+
+${include_all_option_headers}
+
+#line 27 "${template}"
+
+namespace CVC4 {
+namespace options {
+
+struct OptionsHolder {
+  OptionsHolder();
+${all_modules_contributions}
+
+#line 36 "${template}"
+
+};/* struct OptionsHolder */
+
+}/* CVC4::options namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OPTIONS__OPTIONS_HOLDER_H */
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
new file mode 100644
index 000000000..2df69b5d3
--- /dev/null
+++ b/src/options/options_template.cpp
@@ -0,0 +1,471 @@
+/*********************                                                        */
+/*! \file options_template.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** 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 Contains code for handling command-line options.
+ **
+ ** Contains code for handling command-line options
+ **/
+
+#include <cstdio>
+#include <cstdlib>
+#include <new>
+#include <string>
+#include <sstream>
+#include <limits>
+#include <unistd.h>
+#include <string.h>
+#include <stdint.h>
+#include <time.h>
+
+#include <getopt.h>
+
+#include "expr/expr.h"
+#include "util/configuration.h"
+#include "util/exception.h"
+#include "util/language.h"
+
+${include_all_option_headers}
+
+#line 40 "${template}"
+
+#include "util/output.h"
+#include "options/options_holder.h"
+#include "cvc4autoconfig.h"
+#include "options/base_options_handlers.h"
+
+${option_handler_includes}
+
+#line 49 "${template}"
+
+using namespace CVC4;
+using namespace CVC4::options;
+
+namespace CVC4 {
+
+CVC4_THREADLOCAL(Options*) Options::s_current = NULL;
+
+/**
+ * This is a default handler for options of built-in C++ type.  This
+ * template is really just a helper for the handleOption() template,
+ * below.  Variants of this template handle numeric and non-numeric,
+ * integral and non-integral, signed and unsigned C++ types.
+ * handleOption() makes sure to instantiate the right one.
+ *
+ * This implements default behavior when e.g. an option is
+ * unsigned but the user specifies a negative argument; etc.
+ */
+template <class T, bool is_numeric, bool is_integer>
+struct OptionHandler {
+  static T handle(std::string option, std::string optarg);
+};/* struct OptionHandler<> */
+
+/** Variant for integral C++ types */
+template <class T>
+struct OptionHandler<T, true, true> {
+  static T handle(std::string option, std::string optarg) {
+    try {
+      Integer i(optarg, 0);
+
+      if(! std::numeric_limits<T>::is_signed && i < 0) {
+        // unsigned type but user gave negative argument
+        throw OptionException(option + " requires a nonnegative argument");
+      } else if(i < std::numeric_limits<T>::min()) {
+        // negative overflow for type
+        std::stringstream ss;
+        ss << option << " requires an argument >= " << std::numeric_limits<T>::min();
+        throw OptionException(ss.str());
+      } else if(i > std::numeric_limits<T>::max()) {
+        // positive overflow for type
+        std::stringstream ss;
+        ss << option << " requires an argument <= " << std::numeric_limits<T>::max();
+        throw OptionException(ss.str());
+      }
+
+      if(std::numeric_limits<T>::is_signed) {
+        return T(i.getLong());
+      } else {
+        return T(i.getUnsignedLong());
+      }
+    } catch(std::invalid_argument&) {
+      // user gave something other than an integer
+      throw OptionException(option + " requires an integer argument");
+    }
+  }
+};/* struct OptionHandler<T, true, true> */
+
+/** Variant for numeric but non-integral C++ types */
+template <class T>
+struct OptionHandler<T, true, false> {
+  static T handle(std::string option, std::string optarg) {
+    std::stringstream in(optarg);
+    long double r;
+    in >> r;
+    if(! in.eof()) {
+      // we didn't consume the whole string (junk at end)
+      throw OptionException(option + " requires a numeric argument");
+    }
+
+    if(! std::numeric_limits<T>::is_signed && r < 0.0) {
+      // unsigned type but user gave negative value
+      throw OptionException(option + " requires a nonnegative argument");
+    } else if(r < -std::numeric_limits<T>::max()) {
+      // negative overflow for type
+      std::stringstream ss;
+      ss << option << " requires an argument >= " << -std::numeric_limits<T>::max();
+      throw OptionException(ss.str());
+    } else if(r > std::numeric_limits<T>::max()) {
+      // positive overflow for type
+      std::stringstream ss;
+      ss << option << " requires an argument <= " << std::numeric_limits<T>::max();
+      throw OptionException(ss.str());
+    }
+
+    return T(r);
+  }
+};/* struct OptionHandler<T, true, false> */
+
+/** Variant for non-numeric C++ types */
+template <class T>
+struct OptionHandler<T, false, false> {
+  static T handle(std::string option, std::string optarg) {
+    T::unsupported_handleOption_call___please_write_me;
+    // The above line causes a compiler error if this version of the template
+    // is ever instantiated (meaning that a specialization is missing).  So
+    // don't worry about the segfault in the next line, the "return" is only
+    // there to keep the compiler from giving additional, distracting errors
+    // and warnings.
+    return *(T*)0;
+  }
+};/* struct OptionHandler<T, false, false> */
+
+/** Handle an option of type T in the default way. */
+template <class T>
+T handleOption(std::string option, std::string optarg) {
+  return OptionHandler<T, std::numeric_limits<T>::is_specialized, std::numeric_limits<T>::is_integer>::handle(option, optarg);
+}
+
+/** Handle an option of type std::string in the default way. */
+template <>
+std::string handleOption<std::string>(std::string option, std::string optarg) {
+  return optarg;
+}
+
+/**
+ * Run handler, and any user-given predicates, for option T.
+ * If a user specifies a :handler or :predicates, it overrides this.
+ */
+template <class T>
+typename T::type runHandlerAndPredicates(T, std::string option, std::string optarg, SmtEngine* smt) {
+  // By default, parse the option argument in a way appropriate for its type.
+  // E.g., for "unsigned int" options, ensure that the provided argument is
+  // a nonnegative integer that fits in the unsigned int type.
+
+  return handleOption<typename T::type>(option, optarg);
+}
+
+template <class T>
+void runBoolPredicates(T, std::string option, bool b, SmtEngine* smt) {
+  // By default, nothing to do for bool.  Users add things with
+  // :predicate in options files to provide custom checking routines
+  // that can throw exceptions.
+}
+
+${all_custom_handlers}
+
+#line 186 "${template}"
+
+#ifdef CVC4_DEBUG
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true
+#else /* CVC4_DEBUG */
+#  define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false
+#endif /* CVC4_DEBUG */
+
+#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
+#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
+#  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
+#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
+
+Options::Options() :
+  d_holder(new options::OptionsHolder()) {
+}
+
+Options::Options(const Options& options) :
+  d_holder(new options::OptionsHolder(*options.d_holder)) {
+}
+
+Options::~Options() {
+  delete d_holder;
+}
+
+options::OptionsHolder::OptionsHolder() : ${all_modules_defaults}
+{
+}
+
+#line 216 "${template}"
+
+static const std::string mostCommonOptionsDescription = "\
+Most commonly-used CVC4 options:${common_documentation}";
+
+#line 221 "${template}"
+
+static const std::string optionsDescription = mostCommonOptionsDescription + "\n\
+\n\
+Additional CVC4 options:${remaining_documentation}";
+
+#line 227 "${template}"
+
+static const std::string languageDescription = "\
+Languages currently supported as arguments to the -L / --lang option:\n\
+  auto           attempt to automatically determine the input language\n\
+  pl | cvc4      CVC4 presentation language\n\
+  smt | smtlib   SMT-LIB format 1.2\n\
+  smt2 | smtlib2 SMT-LIB format 2.0\n\
+  tptp           TPTP format (cnf and fof)\n\
+\n\
+Languages currently supported as arguments to the --output-lang option:\n\
+  auto           match the output language to the input language\n\
+  pl | cvc4      CVC4 presentation language\n\
+  smt | smtlib   SMT-LIB format 1.2\n\
+  smt2 | smtlib2 SMT-LIB format 2.0\n\
+  tptp           TPTP format\n\
+  ast            internal format (simple syntax-tree language)\n\
+";
+
+std::string Options::getDescription() const {
+  return optionsDescription;
+}
+
+void Options::printUsage(const std::string msg, std::ostream& out) {
+  out << msg << optionsDescription << std::endl << std::flush;
+}
+
+void Options::printShortUsage(const std::string msg, std::ostream& out) {
+  out << msg << mostCommonOptionsDescription << std::endl << std::endl
+      << "For full usage, please use --help." << std::endl << std::flush;
+}
+
+void Options::printLanguageHelp(std::ostream& out) {
+  out << languageDescription << std::flush;
+}
+
+/**
+ * This is a table of long options.  By policy, each short option
+ * should have an equivalent long option (but the reverse isn't the
+ * case), so this table should thus contain all command-line options.
+ *
+ * Each option in this array has four elements:
+ *
+ * 1. the long option string
+ * 2. argument behavior for the option:
+ *    no_argument - no argument permitted
+ *    required_argument - an argument is expected
+ *    optional_argument - an argument is permitted but not required
+ * 3. this is a pointer to an int which is set to the 4th entry of the
+ *    array if the option is present; or NULL, in which case
+ *    getopt_long() returns the 4th entry
+ * 4. the return value for getopt_long() when this long option (or the
+ *    value to set the 3rd entry to; see #3)
+ *
+ * If you add something here, you should add it in src/main/usage.h
+ * also, to document it.
+ *
+ * If you add something that has a short option equivalent, you should
+ * add it to the getopt_long() call in parseOptions().
+ */
+static struct option cmdlineOptions[] = {${all_modules_long_options}
+  { NULL, no_argument, NULL, '\0' }
+};/* cmdlineOptions */
+
+#line 291 "${template}"
+
+static void preemptGetopt(int& argc, char**& argv, const char* opt) {
+  const size_t maxoptlen = 128;
+
+  Debug("preemptGetopt") << "preempting getopt() with " << opt << std::endl;
+
+  AlwaysAssert(opt != NULL && *opt != '\0');
+  AlwaysAssert(strlen(opt) <= maxoptlen);
+
+  ++argc;
+  unsigned i = 1;
+  while(argv[i] != NULL && argv[i][0] != '\0') {
+    ++i;
+  }
+
+  if(argv[i] == NULL) {
+    argv = (char**) realloc(argv, (i + 6) * sizeof(char*));
+    for(unsigned j = i; j < i + 5; ++j) {
+      argv[j] = (char*) malloc(sizeof(char) * maxoptlen);
+      argv[j][0] = '\0';
+    }
+    argv[i + 5] = NULL;
+  }
+
+  strncpy(argv[i], opt, maxoptlen - 1);
+  argv[i][maxoptlen - 1] = '\0'; // ensure NUL-termination even on overflow
+}
+
+namespace options {
+
+/** Set a given Options* as "current" just for a particular scope. */
+class OptionsGuard {
+  Options** d_field;
+  Options* d_old;
+public:
+  OptionsGuard(Options** field, Options* opts) :
+    d_field(field),
+    d_old(*field) {
+    *field = opts;
+  }
+  ~OptionsGuard() {
+    *d_field = d_old;
+  }
+};/* class OptionsGuard */
+
+}/* CVC4::options namespace */
+
+/** Parse argc/argv and put the result into a CVC4::Options. */
+int Options::parseOptions(int argc, char* main_argv[]) throw(OptionException) {
+  options::OptionsGuard guard(&s_current, this);
+
+  const char *progName = main_argv[0];
+  SmtEngine* const smt = NULL;
+
+  // Reset getopt(), in the case of multiple calls to parseOptions().
+  // This can be = 1 in newer GNU getopt, but older (< 2007) require = 0.
+  optind = 0;
+#if HAVE_DECL_OPTRESET
+  optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
+#endif /* HAVE_DECL_OPTRESET */
+
+  // find the base name of the program
+  const char *x = strrchr(progName, '/');
+  if(x != NULL) {
+    progName = x + 1;
+  }
+  d_holder->binary_name = std::string(progName);
+
+  int extra_argc = 1;
+  char **extra_argv = (char**) malloc(2 * sizeof(char*));
+  extra_argv[0] = NULL;
+  extra_argv[1] = NULL;
+
+  int extra_optind = 0, main_optind = 0;
+  int old_optind;
+
+  char** argv = main_argv;
+
+  for(;;) {
+    int c = -1;
+    Debug("preemptGetopt") << "top of loop, extra_optind == " << extra_optind << ", extra_argc == " << extra_argc << std::endl;
+    if((extra_optind == 0 ? 1 : extra_optind) < extra_argc) {
+#if HAVE_DECL_OPTRESET
+      optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
+#endif /* HAVE_DECL_OPTRESET */
+      old_optind = optind = extra_optind;
+      argv = extra_argv;
+      Debug("preemptGetopt") << "in preempt code, next arg is " << extra_argv[optind == 0 ? 1 : optind] << std::endl;
+      c = getopt_long(extra_argc, extra_argv,
+                      ":${all_modules_short_options}",
+                      cmdlineOptions, NULL);
+      Debug("preemptGetopt") << "in preempt code, c == " << c << " (`" << char(c) << "') optind == " << optind << std::endl;
+      if(optind >= extra_argc) {
+        Debug("preemptGetopt") << "-- no more preempt args" << std::endl;
+        unsigned i = 0;
+        while(extra_argv[i] != NULL && extra_argv[i][0] != '\0') {
+          extra_argv[i][0] = '\0';
+          ++i;
+        }
+        extra_argc = 1;
+        extra_optind = 0;
+      } else {
+        Debug("preemptGetopt") << "-- more preempt args" << std::endl;
+        extra_optind = optind;
+      }
+    }
+    if(c == -1) {
+#if HAVE_DECL_OPTRESET
+      optreset = 1; // on BSD getopt() (e.g. Mac OS), might also need this
+#endif /* HAVE_DECL_OPTRESET */
+      old_optind = optind = main_optind;
+      argv = main_argv;
+      c = getopt_long(argc, main_argv,
+                      ":${all_modules_short_options}",
+                      cmdlineOptions, NULL);
+      main_optind = optind;
+      if(c == -1) {
+        break;
+      }
+    }
+
+    Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "')" << std::endl;
+
+    switch(c) {
+${all_modules_option_handlers}
+
+#line 418 "${template}"
+
+    case ':':
+      // This can be a long or short option, and the way to get at the
+      // name of it is different.
+      if(optopt == 0 ||
+         ( optopt >= ${long_option_value_begin} && optopt <= ${long_option_value_end} )) {
+        // was a long option
+        throw OptionException(std::string("option `") + argv[optind - 1] + "' missing its required argument");
+      } else {
+        // was a short option
+        throw OptionException(std::string("option `-") + char(optopt) + "' missing its required argument");
+      }
+
+    case '?':
+    default:
+      if(optopt == 0 &&
+         !strncmp(argv[optind - 1], "--thread", 8) &&
+         strlen(argv[optind - 1]) > 8 &&
+         isdigit(argv[optind - 1][8])) {
+        std::vector<std::string>& threadArgv = d_holder->threadArgv;
+        int tnum = atoi(argv[optind - 1] + 8);
+        threadArgv.resize(tnum + 1);
+        if(threadArgv[tnum] != "") {
+          threadArgv[tnum] += " ";
+        }
+        const char* p = strchr(argv[optind - 1] + 9, '=');
+        if(p == NULL) { // e.g., we have --thread0 "foo"
+          threadArgv[tnum] += argv[optind++];
+        } else { // e.g., we have --thread0="foo"
+          threadArgv[tnum] += p + 1;
+        }
+        break;
+      }
+
+      // This can be a long or short option, and the way to get at the name of it is different.
+      if(optopt == 0) { // was a long option
+        throw OptionException(std::string("can't understand option `") + argv[optind - 1] + "'");
+      } else { // was a short option
+        throw OptionException(std::string("can't understand option `-") + char(optopt) + "'");
+      }
+    }
+  }
+
+  if((*this)[options::incrementalSolving] && (*this)[options::proof]) {
+    throw OptionException(std::string("The use of --incremental with --proof is not yet supported"));
+  }
+
+  return optind;
+}
+
+#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT
+#undef DO_SEMANTIC_CHECKS_BY_DEFAULT
+
+}/* CVC4 namespace */