Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

17 files changed, 2165 insertions, 1060 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 69dc06e47..f7dfdb410 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -14,21 +14,22 @@
  ** [[ Add lengthier description here ]]
  ** \todo document this file
  **/
-
 #include "smt/boolean_terms.h"
+
+#include <algorithm>
+#include <map>
+#include <set>
+#include <stack>
+#include <string>
+
+#include "expr/kind.h"
+#include "expr/node_manager_attributes.h"
+#include "options/boolean_term_conversion_mode.h"
+#include "options/booleans_options.h"
 #include "smt/smt_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
-#include "theory/booleans/boolean_term_conversion_mode.h"
-#include "theory/booleans/options.h"
-#include "expr/kind.h"
-#include "expr/node_manager_attributes.h"
 #include "util/ntuple.h"
-#include <string>
-#include <algorithm>
-#include <set>
-#include <map>
-#include <stack>
 
 using namespace std;
 using namespace CVC4::theory;
diff --git a/src/smt/command_list.cpp b/src/smt/command_list.cpp
index 18a09e7ed..3e912d338 100644
--- a/src/smt/command_list.cpp
+++ b/src/smt/command_list.cpp
@@ -17,8 +17,7 @@
 // we include both of these to make sure they agree on the typedef
 #include "smt/command_list.h"
 #include "smt/smt_engine.h"
-
-#include "expr/command.h"
+#include "smt_util/command.h"
 
 namespace CVC4 {
 namespace smt {
diff --git a/src/smt/logic_exception.h b/src/smt/logic_exception.h
index 8fda9b9e2..a641f8d21 100644
--- a/src/smt/logic_exception.h
+++ b/src/smt/logic_exception.h
@@ -22,7 +22,7 @@
 #ifndef __CVC4__SMT__LOGIC_EXCEPTION_H
 #define __CVC4__SMT__LOGIC_EXCEPTION_H
 
-#include "util/exception.h"
+#include "base/exception.h"
 
 namespace CVC4 {
 
diff --git a/src/smt/modal_exception.h b/src/smt/modal_exception.h
deleted file mode 100644
index 11e78ab19..000000000
--- a/src/smt/modal_exception.h
+++ /dev/null
@@ -1,47 +0,0 @@
-/*********************                                                        */
-/*! \file modal_exception.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief An exception that is thrown when an interactive-only
- ** feature while CVC4 is being used in a non-interactive setting
- **
- ** 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__MODAL_EXCEPTION_H
-#define __CVC4__SMT__MODAL_EXCEPTION_H
-
-#include "util/exception.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC ModalException : public CVC4::Exception {
-public:
-  ModalException() :
-    Exception("Feature used while operating in "
-              "incorrect state") {
-  }
-
-  ModalException(const std::string& msg) :
-    Exception(msg) {
-  }
-
-  ModalException(const char* msg) :
-    Exception(msg) {
-  }
-};/* class ModalException */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__MODAL_EXCEPTION_H */
diff --git a/src/smt/modal_exception.i b/src/smt/modal_exception.i
deleted file mode 100644
index 15b8150cf..000000000
--- a/src/smt/modal_exception.i
+++ /dev/null
@@ -1,7 +0,0 @@
-%{
-#include "smt/modal_exception.h"
-%}
-
-%ignore CVC4::ModalException::ModalException(const char*);
-
-%include "smt/modal_exception.h"
diff --git a/src/smt/options b/src/smt/options
deleted file mode 100644
index 7c725e508..000000000
--- a/src/smt/options
+++ /dev/null
@@ -1,164 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module SMT "smt/options.h" SMT layer
-
-common-option - dump --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
- dump preprocessed assertions, etc., see --dump=help
-common-option - dump-to --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
- all dumping goes to FILE (instead of stdout)
-
-expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo :include "theory/logic_info.h" :handler CVC4::smt::stringToLogicInfo :handler-include "smt/options_handlers.h" :default '""'
- set the logic, and override all further user attempts to change it
-
-option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h"
- choose simplification mode, see --simplification=help
-alias --no-simplification = --simplification=none
- turn off all simplification (same as --simplification=none)
-
-option doStaticLearning static-learning --static-learning bool :default true
- use static learning (on by default)
-
-option expandDefinitions expand-definitions bool :default false
- always expand symbol definitions in output
-common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
- support the get-value and get-model commands
-option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
-option dumpModels --dump-models bool :default false :link --produce-models
- output models after every SAT/INVALID/UNKNOWN response
-option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- turn on proof generation
-option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
- after UNSAT/VALID, machine-check the generated proof
-option dumpProofs --dump-proofs bool :default false :link --proof
- output proofs after every UNSAT/VALID response
-option dumpInstantiations --dump-instantiations bool :default false
- output instantiations of quantified formulas after every UNSAT/VALID response
-option dumpSynth --dump-synth bool :read-write :default false
- output solution for synthesis conjectures after every UNSAT/VALID response
-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- turn on unsat core generation
-option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write
- after UNSAT/VALID, produce and check an unsat core (expensive)
-option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- output unsat cores after every UNSAT/VALID response
-
-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- support the get-assignment command
-
-undocumented-option interactiveMode interactive-mode bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
- deprecated name for produce-assertions
-common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::smt::beforeSearch CVC4::smt::setProduceAssertions :predicate-include "smt/options_handlers.h" :read-write
- keep an assertions list (enables get-assertions command)
-
-option doITESimp --ite-simp bool :read-write
- turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
-
-option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false
- do the ite simplification pass again if repeating simplification
-
-option simplifyWithCareEnabled --simp-with-care bool :default false :read-write
- enables simplifyWithCare in ite simplificiation
-
-option compressItes --simp-ite-compress bool :default false :read-write
- enables compressing ites after ite simplification
-
-option unconstrainedSimp --unconstrained-simp bool :default false :read-write
- turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
-
-option repeatSimp --repeat-simp bool :read-write
- make multiple passes with nonclausal simplifier
-
-option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
- post ite compression enables zombie removal while the number of nodes is above this threshold
-
-option sortInference --sort-inference bool :read-write :default false
- calculate sort inference of input problem, convert the input based on monotonic sorts
-
-common-option incrementalSolving incremental -i --incremental bool :default true
- enable incremental solving
-
-option abstractValues abstract-values --abstract-values bool :default false
- in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
-option modelUninterpDtEnum --model-u-dt-enum bool :default false
- in models, output uninterpreted sorts as datatype enumerations
-
-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 --tlimit=MS "unsigned long" :handler CVC4::smt::tlimitHandler :handler-include "smt/options_handlers.h"
- enable time limiting (give milliseconds)
-common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::smt::tlimitPerHandler :handler-include "smt/options_handlers.h"
- enable time limiting per query (give milliseconds)
-common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::smt::rlimitHandler :handler-include "smt/options_handlers.h"
- enable resource limiting (currently, roughly the number of SAT conflicts)
-common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::smt::rlimitPerHandler :handler-include "smt/options_handlers.h"
- enable resource limiting per query
-common-option hardLimit hard-limit --hard-limit bool :default false
- the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)
-common-option cpuTime cpu-time --cpu-time bool :default false
- measures CPU time if set to true and wall time if false (default false)
-
-# Resource spending options for SPARK
-expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1
- ammount of resources spent for each rewrite step
-
-expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1
- ammount of resources spent for each theory check call
-
-expert-option decisionStep decision-step --decision-step unsigned :default 1
- ammount of getNext decision calls in the decision engine
- 
-expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
- ammount of resources spent for each bitblast step
- 
-expert-option parseStep parse-step --parse-step unsigned :default 1
- ammount of resources spent for each command/expression parsing
- 
-expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
- ammount of resources spent when adding lemmas
- 
-expert-option restartStep restart-step --restart-step unsigned :default 1
- ammount of resources spent for each theory restart
- 
-expert-option cnfStep cnf-step --cnf-step unsigned :default 1
- ammount of resources spent for each call to cnf conversion
- 
-expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
- ammount of resources spent for each preprocessing step in SmtEngine
- 
-expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
- ammount of resources spent for quantifier instantiations
- 
-expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1
- ammount of resources spent for each sat conflict (main sat solver)
- 
-expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
- ammount of resources spent for each sat conflict (bitvectors)
- 
- 
-expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
- eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
-
-# --replay is currently broken; don't document it for 1.0
-undocumented-option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
- replay decisions from file
-undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
- log decisions and propagations to file
-option replayStream ExprStream*
-
-# portfolio options
-option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h"
- The input channel to receive notfication events for new lemmas
-option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
- The output channel to receive notfication events for new lemmas
-
-option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
- Force no CPU limit when dumping models and proofs
-
-endmodule
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
deleted file mode 100644
index eeefd7af0..000000000
--- a/src/smt/options_handlers.h
+++ /dev/null
@@ -1,517 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Custom handlers and predicates for SmtEngine options
- **
- ** Custom handlers and predicates for SmtEngine options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__SMT__OPTIONS_HANDLERS_H
-#define __CVC4__SMT__OPTIONS_HANDLERS_H
-
-#include "cvc4autoconfig.h"
-#include "util/configuration_private.h"
-#include "util/dump.h"
-#include "util/resource_manager.h"
-#include "smt/modal_exception.h"
-#include "smt/smt_engine.h"
-#include "lib/strtok_r.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\
-benchmark\n\
-+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
-  does not include any declarations or assertions.  Implied by all following\n\
-  modes.\n\
-\n\
-declarations\n\
-+ Dump user declarations.  Implied by all following modes.\n\
-\n\
-skolems\n\
-+ Dump internally-created skolem variable declarations.  These can\n\
-  arise from preprocessing simplifications, existential elimination,\n\
-  and a number of other things.  Implied by all following modes.\n\
-\n\
-assertions\n\
-+ Output the assertions after preprocessing and before clausification.\n\
-  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
-  where PASS is one of the preprocessing passes: definition-expansion\n\
-  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
-  simplify static-learning ite-removal repeat-simplify\n\
-  rewrite-apply-to-const theory-preprocessing.\n\
-  PASS can also be the special value \"everything\", in which case the\n\
-  assertions are printed before any preprocessing (with\n\
-  \"assertions:pre-everything\") or after all preprocessing completes\n\
-  (with \"assertions:post-everything\").\n\
-\n\
-clauses\n\
-+ Do all the preprocessing outlined above, and dump the CNF-converted\n\
-  output\n\
-\n\
-state\n\
-+ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
-  Implied by all \"stateful\" modes below and conflicts with all\n\
-  non-stateful modes below.\n\
-\n\
-t-conflicts [non-stateful]\n\
-+ Output correctness queries for all theory conflicts\n\
-\n\
-missed-t-conflicts [stateful]\n\
-+ Output completeness queries for theory conflicts\n\
-\n\
-t-propagations [stateful]\n\
-+ Output correctness queries for all theory propagations\n\
-\n\
-missed-t-propagations [stateful]\n\
-+ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
-\n\
-t-lemmas [non-stateful]\n\
-+ Output correctness queries for all theory lemmas\n\
-\n\
-t-explanations [non-stateful]\n\
-+ Output correctness queries for all theory explanations\n\
-\n\
-bv-rewrites [non-stateful]\n\
-+ Output correctness queries for all bitvector rewrites\n\
-\n\
-bv-abstraction [non-stateful]\n\
-+ Output correctness queries for all bv abstraction \n\
-\n\
-bv-algebraic [non-stateful]\n\
-+ Output correctness queries for bv algebraic solver. \n\
-\n\
-theory::fullcheck [non-stateful]\n                                      \
-+ Output completeness queries for all full-check effort-level theory checks\n\
-\n\
-Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
-one from the assertions category (either assertions or clauses), and\n\
-perhaps one or more stateful or non-stateful modes for checking correctness\n\
-and completeness of decision procedure implementations.  Stateful modes dump\n\
-the contextual assertions made by the core solver (all decisions and\n\
-propagations as assertions; that affects the validity of the resulting\n\
-correctness and completeness queries, so of course stateful and non-stateful\n\
-modes cannot be mixed in the same run.\n\
-\n\
-The --output-language option controls the language used for dumping, and\n\
-this allows you to connect CVC4 to another solver implementation via a UNIX\n\
-pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
-to a file.\n\
-";
-
-static const std::string simplificationHelp = "\
-Simplification modes currently supported by the --simplification option:\n\
-\n\
-batch (default) \n\
-+ save up all ASSERTions; run nonclausal simplification and clausal\n\
-  (MiniSat) propagation for all of them only after reaching a querying command\n\
-  (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
-\n\
-none\n\
-+ do not perform nonclausal simplification\n\
-";
-
-inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
-#ifdef CVC4_DUMPING
-  char* optargPtr = strdup(optarg.c_str());
-  char* tokstr = optargPtr;
-  char* toksave;
-  while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
-    tokstr = NULL;
-    if(!strcmp(optargPtr, "benchmark")) {
-    } else if(!strcmp(optargPtr, "declarations")) {
-    } else if(!strcmp(optargPtr, "assertions")) {
-      Dump.on("assertions:post-everything");
-    } else if(!strncmp(optargPtr, "assertions:", 11)) {
-      const char* p = optargPtr + 11;
-      if(!strncmp(p, "pre-", 4)) {
-        p += 4;
-      } else if(!strncmp(p, "post-", 5)) {
-        p += 5;
-      } else {
-        throw OptionException(std::string("don't know how to dump `") +
-                              optargPtr + "'.  Please consult --dump help.");
-      }
-      if(!strcmp(p, "everything")) {
-      } else if(!strcmp(p, "definition-expansion")) {
-      } else if(!strcmp(p, "boolean-terms")) {
-      } else if(!strcmp(p, "constrain-subtypes")) {
-      } else if(!strcmp(p, "substitution")) {
-      } else if(!strcmp(p, "strings-pp")) {
-      } else if(!strcmp(p, "skolem-quant")) {
-      } else if(!strcmp(p, "simplify")) {
-      } else if(!strcmp(p, "static-learning")) {
-      } else if(!strcmp(p, "ite-removal")) {
-      } else if(!strcmp(p, "repeat-simplify")) {
-      } else if(!strcmp(p, "rewrite-apply-to-const")) {
-      } else if(!strcmp(p, "theory-preprocessing")) {
-      } else if(!strcmp(p, "nonclausal")) {
-      } else if(!strcmp(p, "theorypp")) {
-      } else if(!strcmp(p, "itesimp")) {
-      } else if(!strcmp(p, "unconstrained")) {
-      } else if(!strcmp(p, "repeatsimp")) {
-      } else {
-        throw OptionException(std::string("don't know how to dump `") +
-                              optargPtr + "'.  Please consult --dump help.");
-      }
-      Dump.on("assertions");
-    } else if(!strcmp(optargPtr, "skolems")) {
-    } else if(!strcmp(optargPtr, "clauses")) {
-    } else if(!strcmp(optargPtr, "t-conflicts") ||
-              !strcmp(optargPtr, "t-lemmas") ||
-              !strcmp(optargPtr, "t-explanations") ||
-              !strcmp(optargPtr, "bv-rewrites") ||
-              !strcmp(optargPtr, "theory::fullcheck")) {
-      // These are "non-state-dumping" modes.  If state (SAT decisions,
-      // propagations, etc.) is dumped, it will interfere with the validity
-      // of these generated queries.
-      if(Dump.isOn("state")) {
-        throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-      } else {
-        Dump.on("no-permit-state");
-      }
-    } else if(!strcmp(optargPtr, "state") ||
-              !strcmp(optargPtr, "missed-t-conflicts") ||
-              !strcmp(optargPtr, "t-propagations") ||
-              !strcmp(optargPtr, "missed-t-propagations")) {
-      // These are "state-dumping" modes.  If state (SAT decisions,
-      // propagations, etc.) is not dumped, it will interfere with the
-      // validity of these generated queries.
-      if(Dump.isOn("no-permit-state")) {
-        throw OptionException(std::string("dump option `") + optargPtr +
-                              "' conflicts with a previous, "
-                              "non-state-dumping dump option.  You cannot "
-                              "mix stateful and non-stateful dumping modes; "
-                              "see --dump help.");
-      } else {
-        Dump.on("state");
-      }
-    } else if(!strcmp(optargPtr, "help")) {
-      puts(dumpHelp.c_str());
-      exit(1);
-    } else if(!strcmp(optargPtr, "bv-abstraction")) {
-      Dump.on("bv-abstraction");
-    } else if(!strcmp(optargPtr, "bv-algebraic")) {
-      Dump.on("bv-algebraic");
-    } else {
-      throw OptionException(std::string("unknown option for --dump: `") +
-                            optargPtr + "'.  Try --dump help.");
-    }
-
-    Dump.on(optargPtr);
-    Dump.on("benchmark");
-    if(strcmp(optargPtr, "benchmark")) {
-      Dump.on("declarations");
-      if(strcmp(optargPtr, "declarations")) {
-        Dump.on("skolems");
-      }
-    }
-  }
-  free(optargPtr);
-#else /* CVC4_DUMPING */
-  throw OptionException("The dumping feature was disabled in this build of CVC4.");
-#endif /* CVC4_DUMPING */
-}
-
-inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  try {
-    LogicInfo logic(optarg);
-    if(smt != NULL) {
-      smt->setLogic(logic);
-    }
-    return logic;
-  } catch(IllegalArgumentException& e) {
-    throw OptionException(std::string("invalid logic specification for --force-logic: `") +
-                          optarg + "':\n" + e.what());
-  }
-}
-
-inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "batch") {
-    return SIMPLIFICATION_MODE_BATCH;
-  } 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.");
-  }
-}
-
-// ensure we haven't started search yet
-inline void beforeSearch(std::string option, bool value, SmtEngine* smt) throw(ModalException) {
-  if(smt != NULL && smt->d_fullyInited) {
-    std::stringstream ss;
-    ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)";
-    throw ModalException(ss.str());
-  }
-}
-
-inline void setProduceAssertions(std::string option, bool value, SmtEngine* smt) throw() {
-  options::produceAssertions.set(value);
-  options::interactiveMode.set(value);
-}
-
-// ensure we are a proof-enabled build of CVC4
-inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-#if !(IS_PROOFS_BUILD)
-  if(value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
-    throw OptionException(ss.str());
-  }
-#endif /* IS_PROOFS_BUILD */
-}
-
-// 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
-  std::ostream* outStream = NULL;
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name for --dump-to"));
-  } else if(optarg == "-") {
-    outStream = &DumpOutC::dump_cout;
-  } else if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } 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 dump-to file: `" << optarg << "': " << __cvc4_errno_failreason();
-      throw OptionException(ss.str());
-    }
-  }
-  __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 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 if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } 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 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 if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } 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 == "") {
-    throw OptionException(std::string("Bad file name for --replay"));
-  } else {
-    return optarg;
-  }
-#else /* CVC4_REPLAY */
-  throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
-
-inline std::ostream* checkReplayLogFilename(std::string option, std::string optarg, SmtEngine* smt) {
-#ifdef CVC4_REPLAY
-  if(optarg == "") {
-    throw OptionException(std::string("Bad file name for --replay-log"));
-  } else if(optarg == "-") {
-    return &std::cout;
-  } else if(!options::filesystemAccess()) {
-    throw OptionException(std::string("Filesystem access not permitted"));
-  } else {
-    errno = 0;
-    std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
-    if(replayLog == NULL || !*replayLog) {
-      std::stringstream ss;
-      ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
-      throw OptionException(ss.str());
-    }
-    return replayLog;
-  }
-#else /* CVC4_REPLAY */
-  throw OptionException("The replay feature was disabled in this build of CVC4.");
-#endif /* CVC4_REPLAY */
-}
-
-// ensure we are a stats-enabled build of CVC4
-inline void statsEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-#ifndef CVC4_STATISTICS_ON
-  if(value) {
-    std::stringstream ss;
-    ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
-    throw OptionException(ss.str());
-  }
-#endif /* CVC4_STATISTICS_ON */
-}
-
-inline unsigned long tlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  // make sure the resource is set if the option is updated
-  // if the smt engine is null the resource will be set in the
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setTimeLimit(ms, true);
-  }
-  return ms;
-}
-
-inline unsigned long tlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setTimeLimit(ms, false);
-  }
-  return ms;
-}
-
-inline unsigned long rlimitHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setResourceLimit(ms, true);
-  }
-  return ms;
-}
-
-inline unsigned long rlimitPerHandler(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  unsigned long ms;
-
-  std::istringstream convert(optarg);
-  if (!(convert >> ms))
-    throw OptionException("option `"+option+"` requires a number as an argument");
-
-  if (smt != NULL) {
-    ResourceManager* rm = NodeManager::fromExprManager(smt->getExprManager())->getResourceManager();
-    rm->setResourceLimit(ms, false);
-  }
-  return ms;
-}
-
-}/* CVC4::smt namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__OPTIONS_HANDLERS_H */
diff --git a/src/smt/simplification_mode.cpp b/src/smt/simplification_mode.cpp
deleted file mode 100644
index be46badfc..000000000
--- a/src/smt/simplification_mode.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file simplification_mode.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** 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
- **/
-
-#include "smt/simplification_mode.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
-  switch(mode) {
-  case SIMPLIFICATION_MODE_BATCH:
-    out << "SIMPLIFICATION_MODE_BATCH";
-    break;
-  case SIMPLIFICATION_MODE_NONE:
-    out << "SIMPLIFICATION_MODE_NONE";
-    break;
-  default:
-    out << "SimplificationMode:UNKNOWN![" << unsigned(mode) << "]";
-  }
-
-  return out;
-}
-
-}/* CVC4 namespace */
diff --git a/src/smt/simplification_mode.h b/src/smt/simplification_mode.h
deleted file mode 100644
index b0b78d318..000000000
--- a/src/smt/simplification_mode.h
+++ /dev/null
@@ -1,39 +0,0 @@
-/*********************                                                        */
-/*! \file simplification_mode.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** 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
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H
-#define __CVC4__SMT__SIMPLIFICATION_MODE_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-/** Enumeration of simplification modes (when to simplify). */
-typedef enum {
-  /** Simplify the assertions all together once a check is requested */
-  SIMPLIFICATION_MODE_BATCH,
-  /** Don't do simplification */
-  SIMPLIFICATION_MODE_NONE
-} SimplificationMode;
-
-std::ostream& operator<<(std::ostream& out, SimplificationMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__SIMPLIFICATION_MODE_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4136c3163..21d190d0e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -14,86 +14,89 @@
  ** The main entry point into the CVC4 library's SMT interface.
  **/
 
-#include <vector>
-#include <string>
+#include "smt/smt_engine.h"
+
+#include <algorithm>
+#include <cctype>
+#include <ext/hash_map>
 #include <iterator>
-#include <utility>
 #include <sstream>
 #include <stack>
-#include <cctype>
-#include <algorithm>
-#include <ext/hash_map>
+#include <string>
+#include <utility>
+#include <vector>
 
-#include "context/cdlist.h"
+#include "options/boolean_term_conversion_mode.h"
+#include "options/decision_mode.h"
+#include "base/exception.h"
+#include "base/modal_exception.h"
+#include "options/option_exception.h"
+#include "base/output.h"
 #include "context/cdhashset.h"
+#include "context/cdlist.h"
 #include "context/context.h"
 #include "decision/decision_engine.h"
-#include "decision/decision_mode.h"
-#include "decision/options.h"
-#include "expr/command.h"
+#include "expr/attribute.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
 #include "expr/metakind.h"
-#include "expr/node_builder.h"
 #include "expr/node.h"
+#include "expr/node_builder.h"
 #include "expr/node_self_iterator.h"
-#include "expr/attribute.h"
-#include "prop/prop_engine.h"
-#include "proof/theory_proof.h"
-#include "smt/modal_exception.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/model_postprocessor.h"
-#include "smt/logic_request.h"
-#include "theory/theory_engine.h"
-#include "theory/bv/theory_bv_rewriter.h"
-#include "proof/proof_manager.h"
-#include "main/options.h"
-#include "util/unsat_core.h"
-#include "util/proof.h"
-#include "util/resource_manager.h"
+#include "expr/resource_manager.h"
+#include "options/arith_options.h"
+#include "options/arrays_options.h"
+#include "options/booleans_options.h"
+#include "options/booleans_options.h"
+#include "options/bv_options.h"
+#include "options/datatypes_options.h"
+#include "options/decision_options.h"
+#include "options/main_options.h"
+#include "options/options_handler_interface.h"
+#include "options/printer_options.h"
+#include "options/prop_options.h"
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "options/strings_options.h"
+#include "options/theory_options.h"
+#include "options/uf_options.h"
+#include "printer/printer.h"
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
-#include "util/boolean_simplification.h"
-#include "util/node_visitor.h"
-#include "util/configuration.h"
-#include "util/configuration_private.h"
-#include "util/exception.h"
-#include "util/nary_builder.h"
-#include "smt/command_list.h"
+#include "proof/proof_manager.h"
+#include "proof/unsat_core.h"
+#include "proof/theory_proof.h"
+#include "prop/prop_engine.h"
 #include "smt/boolean_terms.h"
-#include "smt/options.h"
-#include "options/option_exception.h"
-#include "util/output.h"
-#include "util/hash.h"
-#include "theory/substitutions.h"
-#include "theory/uf/options.h"
-#include "theory/arith/options.h"
-#include "theory/strings/options.h"
-#include "theory/bv/options.h"
-#include "theory/theory_traits.h"
-#include "theory/logic_info.h"
-#include "theory/options.h"
+#include "smt/command_list.h"
+#include "smt/logic_request.h"
+#include "smt/model_postprocessor.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_options_handler.h"
+#include "smt_util/command.h"
+#include "smt_util/boolean_simplification.h"
+#include "smt_util/ite_removal.h"
+#include "smt_util/nary_builder.h"
+#include "smt_util/node_visitor.h"
+#include "theory/arith/pseudoboolean_proc.h"
 #include "theory/booleans/circuit_propagator.h"
-#include "theory/booleans/boolean_term_conversion_mode.h"
-#include "theory/booleans/options.h"
-#include "util/ite_removal.h"
-#include "theory/theory_model.h"
-#include "printer/printer.h"
-#include "prop/options.h"
-#include "theory/arrays/options.h"
-#include "util/sort_inference.h"
-#include "theory/quantifiers/macros.h"
+#include "theory/bv/bvintropow2.h"
+#include "theory/bv/theory_bv_rewriter.h"
+#include "theory/logic_info.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/fun_def_process.h"
+#include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
-#include "theory/quantifiers/ce_guided_instantiation.h"
-#include "theory/quantifiers/options.h"
-#include "theory/datatypes/options.h"
+#include "theory/sort_inference.h"
 #include "theory/strings/theory_strings.h"
-#include "printer/options.h"
-
-#include "theory/arith/pseudoboolean_proc.h"
-#include "theory/bv/bvintropow2.h"
+#include "theory/substitutions.h"
+#include "theory/theory_engine.h"
+#include "theory/theory_model.h"
+#include "theory/theory_traits.h"
+#include "util/configuration.h"
+#include "util/configuration_private.h"
+#include "util/hash.h"
+#include "util/proof.h"
 
 using namespace std;
 using namespace CVC4;
@@ -712,6 +715,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_needPostsolve(false),
   d_earlyTheoryPP(true),
   d_status(),
+  d_optionsHandler(new SmtOptionsHandler(this)),
   d_private(NULL),
   d_smtAttributes(NULL),
   d_statisticsRegistry(NULL),
@@ -884,6 +888,9 @@ SmtEngine::~SmtEngine() throw() {
     delete d_statisticsRegistry;
     d_statisticsRegistry = NULL;
 
+    delete d_optionsHandler;
+    d_optionsHandler = NULL;
+
     delete d_private;
     d_private = NULL;
 
@@ -934,7 +941,7 @@ void SmtEngine::setLogicInternal() throw() {
 
 void SmtEngine::setDefaults() {
   if(options::forceLogic.wasSetByUser()) {
-    d_logic = options::forceLogic();
+    d_logic = *(options::forceLogic());
   }
 
   // set strings-exp
@@ -1596,6 +1603,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   SmtScope smts(this);
 
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
+
   if(Dump.isOn("benchmark")) {
     if(key == "status") {
       string s = value.getValue();
@@ -1700,29 +1708,29 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
       v.push_back((*i).second);
       stats.push_back(v);
     }
-    return stats;
+    return SExpr(stats);
   } else if(key == "error-behavior") {
     // immediate-exit | continued-execution
     if( options::continuedExecution() || options::interactive() ) {
-      return SExpr::Keyword("continued-execution");
+      return SExpr(SExpr::Keyword("continued-execution"));
     } else {
-      return SExpr::Keyword("immediate-exit");
+      return SExpr(SExpr::Keyword("immediate-exit"));
     }
   } else if(key == "name") {
-    return Configuration::getName();
+    return SExpr(Configuration::getName());
   } else if(key == "version") {
-    return Configuration::getVersionString();
+    return SExpr(Configuration::getVersionString());
   } else if(key == "authors") {
-    return Configuration::about();
+    return SExpr(Configuration::about());
   } else if(key == "status") {
     // sat | unsat | unknown
     switch(d_status.asSatisfiabilityResult().isSat()) {
     case Result::SAT:
-      return SExpr::Keyword("sat");
+      return SExpr(SExpr::Keyword("sat"));
     case Result::UNSAT:
-      return SExpr::Keyword("unsat");
+      return SExpr(SExpr::Keyword("unsat"));
     default:
-      return SExpr::Keyword("unknown");
+      return SExpr(SExpr::Keyword("unknown"));
     }
   } else if(key == "reason-unknown") {
     if(!d_status.isNull() && d_status.isUnknown()) {
@@ -1730,7 +1738,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
       ss << d_status.whyUnknown();
       string s = ss.str();
       transform(s.begin(), s.end(), s.begin(), ::tolower);
-      return SExpr::Keyword(s);
+      return SExpr(SExpr::Keyword(s));
     } else {
       throw ModalException("Can't get-info :reason-unknown when the "
                            "last result wasn't unknown!");
@@ -1739,7 +1747,8 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
     return SExpr(d_userLevels.size());
   } else if(key == "all-options") {
     // get the options, like all-statistics
-    return Options::current()->getOptions();
+    std::vector< std::vector<std::string> > current_options = Options::current()->getOptions();
+    return SExpr::parseListOfListOfAtoms(current_options);
   } else {
     throw UnrecognizedOptionException();
   }
@@ -4068,13 +4077,13 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, UnsafeInterruptExce
     vector<SExpr> v;
     if((*i).getKind() == kind::APPLY) {
       Assert((*i).getNumChildren() == 0);
-      v.push_back(SExpr::Keyword((*i).getOperator().toString()));
+      v.push_back(SExpr(SExpr::Keyword((*i).getOperator().toString())));
     } else {
       Assert((*i).isVar());
-      v.push_back(SExpr::Keyword((*i).toString()));
+      v.push_back(SExpr(SExpr::Keyword((*i).toString())));
     }
-    v.push_back(SExpr::Keyword(resultNode.toString()));
-    sexprs.push_back(v);
+    v.push_back(SExpr(SExpr::Keyword(resultNode.toString())));
+    sexprs.push_back(SExpr(v));
   }
   return SExpr(sexprs);
 }
@@ -4669,4 +4678,108 @@ void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
   }
 }
 
+
+
+void SmtEngine::beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException) {
+  if(smt != NULL && smt->d_fullyInited) {
+    std::stringstream ss;
+    ss << "cannot change option `" << option << "' after final initialization (i.e., after logic has been set)";
+    throw ModalException(ss.str());
+  }
+}
+
+
+void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
+  throw(OptionException, ModalException) {
+
+  NodeManagerScope nms(d_nodeManager);
+  Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
+
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << SetOptionCommand(key, value);
+  }
+
+  if(key == "command-verbosity") {
+    if(!value.isAtom()) {
+      const vector<SExpr>& cs = value.getChildren();
+      if(cs.size() == 2 &&
+         (cs[0].isKeyword() || cs[0].isString()) &&
+         cs[1].isInteger()) {
+        string c = cs[0].getValue();
+        const Integer& v = cs[1].getIntegerValue();
+        if(v < 0 || v > 2) {
+          throw OptionException("command-verbosity must be 0, 1, or 2");
+        }
+        d_commandVerbosity[c] = v;
+        return;
+      }
+    }
+    throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
+  }
+
+  if(!value.isAtom()) {
+    throw OptionException("bad value for :" + key);
+  }
+
+  string optionarg = value.getValue();
+
+  d_optionsHandler->setOption(key, optionarg);
+}
+
+CVC4::SExpr SmtEngine::getOption(const std::string& key) const
+  throw(OptionException) {
+
+  NodeManagerScope nms(d_nodeManager);
+
+  Trace("smt") << "SMT getOption(" << key << ")" << endl;
+
+  if(key.length() >= 18 &&
+     key.compare(0, 18, "command-verbosity:") == 0) {
+    map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18);
+    if(i != d_commandVerbosity.end()) {
+      return SExpr((*i).second);
+    }
+    i = d_commandVerbosity.find("*");
+    if(i != d_commandVerbosity.end()) {
+      return SExpr((*i).second);
+    }
+    return SExpr(Integer(2));
+  }
+
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << GetOptionCommand(key);
+  }
+
+  if(key == "command-verbosity") {
+    vector<SExpr> result;
+    SExpr defaultVerbosity;
+    for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
+        i != d_commandVerbosity.end();
+        ++i) {
+      vector<SExpr> v;
+      v.push_back(SExpr((*i).first));
+      v.push_back(SExpr((*i).second));
+      if((*i).first == "*") {
+        // put the default at the end of the SExpr
+        defaultVerbosity = SExpr(v);
+      } else {
+        result.push_back(SExpr(v));
+      }
+    }
+    // put the default at the end of the SExpr
+    if(!defaultVerbosity.isAtom()) {
+      result.push_back(defaultVerbosity);
+    } else {
+      // ensure the default is always listed
+      vector<SExpr> v;
+      v.push_back(SExpr("*"));
+      v.push_back(SExpr(Integer(2)));
+      result.push_back(SExpr(v));
+    }
+    return SExpr(result);
+  }
+
+  return SExpr::parseAtom(d_optionsHandler->getOption(key));
+}
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index be31d768b..c94646c40 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -22,22 +22,22 @@
 #include <string>
 #include <vector>
 
-#include "context/cdlist_forward.h"
+#include "base/modal_exception.h"
 #include "context/cdhashmap_forward.h"
 #include "context/cdhashset_forward.h"
+#include "context/cdlist_forward.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
-#include "util/proof.h"
-#include "util/unsat_core.h"
-#include "smt/modal_exception.h"
-#include "smt/logic_exception.h"
+#include "expr/result.h"
+#include "expr/sexpr.h"
+#include "expr/statistics.h"
 #include "options/options.h"
-#include "util/result.h"
-#include "util/sexpr.h"
+#include "proof/unsat_core.h"
+#include "smt/logic_exception.h"
+#include "theory/logic_info.h"
 #include "util/hash.h"
+#include "util/proof.h"
 #include "util/unsafe_interrupt_exception.h"
-#include "util/statistics.h"
-#include "theory/logic_info.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -72,6 +72,10 @@ namespace prop {
   class PropEngine;
 }/* CVC4::prop namespace */
 
+namespace options {
+  class OptionsHandler;
+}/* CVC4::prop namespace */
+
 namespace expr {
   namespace attr {
     class AttributeManager;
@@ -93,7 +97,6 @@ namespace smt {
   class SmtScope;
   class BooleanTermConverter;
 
-  void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   ProofManager* currentProofManager();
 
   struct CommandCleanup;
@@ -264,6 +267,11 @@ class CVC4_PUBLIC SmtEngine {
   std::map<std::string, Integer> d_commandVerbosity;
 
   /**
+   * This responds to requests to set options.
+   */
+  options::OptionsHandler* d_optionsHandler;
+
+  /**
    * A private utility class to SmtEngine.
    */
   smt::SmtEnginePrivate* d_private;
@@ -354,7 +362,6 @@ class CVC4_PUBLIC SmtEngine {
   friend class ::CVC4::smt::SmtScope;
   friend class ::CVC4::smt::BooleanTermConverter;
   friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
-  friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
   friend ProofManager* ::CVC4::smt::currentProofManager();
   friend class ::CVC4::LogicRequest;
   // to access d_modelCommands
@@ -717,6 +724,11 @@ public:
    */
   void setPrintFuncInModel(Expr f, bool p);
 
+
+  /**
+   * Throws a ModalException if smt is non-null and the SmtEngine has not been fully initialized.
+   */
+  static void beforeSearch(SmtEngine* smt, const std::string& option) throw(ModalException);
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 9cf4467a8..443e4cc58 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -46,7 +46,6 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
 
 %ignore CVC4::SmtEngine::setLogic(const char*);
 %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
-%ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*);
 %ignore CVC4::smt::currentProofManager();
 
 %include "smt/smt_engine.h"
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index d04daef92..2add88afb 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -15,16 +15,18 @@
  ** \todo document this file
  **/
 
-#include "smt/smt_engine.h"
-#include "util/configuration_private.h"
-#include "util/statistics_registry.h"
-#include "check.h"
+#include <unistd.h>
 
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
 #include <string>
-#include <unistd.h>
+
+#include "base/output.h"
+#include "check.h"
+#include "expr/statistics_registry.h"
+#include "smt/smt_engine.h"
+#include "util/configuration_private.h"
 
 using namespace CVC4;
 using namespace std;
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index bc978b728..1dd69abc9 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -19,13 +19,14 @@
 
 #pragma once
 
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "base/tls.h"
 #include "expr/node_manager.h"
+#include "options/smt_options.h"
 #include "smt/smt_engine.h"
-#include "smt/options.h"
 #include "util/configuration_private.h"
-#include "util/cvc4_assert.h"
-#include "util/output.h"
-#include "util/tls.h"
+
 
 namespace CVC4 {
 
diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp
new file mode 100644
index 000000000..3dc5720ab
--- /dev/null
+++ b/src/smt/smt_options_handler.cpp
@@ -0,0 +1,1729 @@
+/*********************                                                        */
+/*! \file options_handler_interface.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Interface for custom handlers and predicates options.
+ **
+ ** Interface for custom handlers and predicates options.
+ **/
+
+#include "smt/smt_options_handler.h"
+
+#include <cerrno>
+#include <cstring>
+#include <ostream>
+#include <sstream>
+#include <string>
+
+#include "base/modal_exception.h"
+#include "base/output.h"
+#include "cvc4autoconfig.h"
+#include "expr/metakind.h"
+#include "expr/node_manager.h"
+#include "expr/resource_manager.h"
+#include "lib/strtok_r.h"
+#include "options/arith_heuristic_pivot_rule.h"
+#include "options/arith_propagation_mode.h"
+#include "options/arith_unate_lemma_mode.h"
+#include "options/boolean_term_conversion_mode.h"
+#include "options/bv_bitblast_mode.h"
+#include "options/bv_options.h"
+#include "options/decision_mode.h"
+#include "options/decision_options.h"
+#include "options/didyoumean.h"
+#include "options/language.h"
+#include "options/main_options.h"
+#include "options/option_exception.h"
+#include "options/options_handler_interface.h"
+#include "options/parser_options.h"
+#include "options/printer_modes.h"
+#include "options/quantifiers_modes.h"
+#include "options/simplification_mode.h"
+#include "options/smt_options.h"
+#include "options/theory_options.h"
+#include "options/theoryof_mode.h"
+#include "options/ufss_mode.h"
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
+#include "smt_util/dump.h"
+#include "theory/logic_info.h"
+#include "util/configuration.h"
+#include "util/configuration_private.h"
+
+
+#warning "TODO: Make SmtOptionsHandler non-public and refactor driver unified."
+
+namespace CVC4 {
+namespace smt {
+
+SmtOptionsHandler::SmtOptionsHandler(SmtEngine* smt)
+    : d_smtEngine(smt)
+{}
+
+SmtOptionsHandler::~SmtOptionsHandler(){}
+
+// theory/arith/options_handlers.h
+const std::string SmtOptionsHandler::s_arithUnateLemmasHelp = "\
+Unate lemmas are generated before SAT search begins using the relationship\n\
+of constant terms and polynomials.\n\
+Modes currently supported by the --unate-lemmas option:\n\
++ none \n\
++ ineqs \n\
+  Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
++ eqs \n\
+  Outputs lemmas of the general forms\n\
+  (= p c) implies (<= p d) for c < d, or\n\
+  (= p c) implies (not (= p d)) for c != d.\n\
++ all \n\
+  A combination of inequalities and equalities.\n\
+";
+
+const std::string SmtOptionsHandler::s_arithPropagationModeHelp = "\
+This decides on kind of propagation arithmetic attempts to do during the search.\n\
++ none\n\
++ unate\n\
+ use constraints to do unate propagation\n\
++ bi (Bounds Inference)\n\
+  infers bounds on basic variables using the upper and lower bounds of the\n\
+  non-basic variables in the tableau.\n\
++both\n\
+";
+
+const std::string SmtOptionsHandler::s_errorSelectionRulesHelp = "\
+This decides on the rule used by simplex during heuristic rounds\n\
+for deciding the next basic variable to select.\n\
+Heuristic pivot rules available:\n\
++min\n\
+  The minimum abs() value of the variable's violation of its bound. (default)\n\
++max\n\
+  The maximum violation the bound\n\
++varord\n\
+  The variable order\n\
+";
+
+ArithUnateLemmaMode SmtOptionsHandler::stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "all") {
+    return ALL_PRESOLVE_LEMMAS;
+  } else if(optarg == "none") {
+    return NO_PRESOLVE_LEMMAS;
+  } else if(optarg == "ineqs") {
+    return INEQUALITY_PRESOLVE_LEMMAS;
+  } else if(optarg == "eqs") {
+    return EQUALITY_PRESOLVE_LEMMAS;
+  } else if(optarg == "help") {
+    puts(s_arithUnateLemmasHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --unate-lemmas: `") +
+                          optarg + "'.  Try --unate-lemmas help.");
+  }
+}
+
+ArithPropagationMode SmtOptionsHandler::stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none") {
+    return NO_PROP;
+  } else if(optarg == "unate") {
+    return UNATE_PROP;
+  } else if(optarg == "bi") {
+    return BOUND_INFERENCE_PROP;
+  } else if(optarg == "both") {
+    return BOTH_PROP;
+  } else if(optarg == "help") {
+    puts(s_arithPropagationModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --arith-prop: `") +
+                          optarg + "'.  Try --arith-prop help.");
+  }
+}
+
+ErrorSelectionRule SmtOptionsHandler::stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "min") {
+    return MINIMUM_AMOUNT;
+  } else if(optarg == "varord") {
+    return VAR_ORDER;
+  } else if(optarg == "max") {
+    return MAXIMUM_AMOUNT;
+  } else if(optarg == "help") {
+    puts(s_errorSelectionRulesHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") +
+                          optarg + "'.  Try --heuristic-pivot-rule help.");
+  }
+}
+
+// theory/quantifiers/options_handlers.h
+
+const std::string SmtOptionsHandler::s_instWhenHelp = "\
+Modes currently supported by the --inst-when option:\n\
+\n\
+full-last-call (default)\n\
++ Alternate running instantiation rounds at full effort and last\n\
+  call.  In other words, interleave instantiation and theory combination.\n\
+\n\
+full\n\
++ Run instantiation round at full effort, before theory combination.\n\
+\n\
+full-delay \n\
++ Run instantiation round at full effort, before theory combination, after\n\
+  all other theories have finished.\n\
+\n\
+full-delay-last-call \n\
++ Alternate running instantiation rounds at full effort after all other\n\
+  theories have finished, and last call.  \n\
+\n\
+last-call\n\
++ Run instantiation at last call effort, after theory combination and\n\
+  and theories report sat.\n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_literalMatchHelp = "\
+Literal match modes currently supported by the --literal-match option:\n\
+\n\
+none (default)\n\
++ Do not use literal matching.\n\
+\n\
+predicate\n\
++ Consider the phase requirements of predicate literals when applying heuristic\n\
+  quantifier instantiation.  For example, the trigger P( x ) in the quantified \n\
+  formula forall( x ). ( P( x ) V ~Q( x ) ) will only be matched with ground\n\
+  terms P( t ) where P( t ) is in the equivalence class of false, and likewise\n\
+  Q( x ) with Q( s ) where Q( s ) is in the equivalence class of true.\n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_mbqiModeHelp = "\
+Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\
+\n\
+default \n\
++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability \n\
+  Modulo Theories.\n\
+\n\
+none \n\
++ Disable model-based quantifier instantiation.\n\
+\n\
+gen-ev \n\
++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper based on generalizing evaluations.\n\
+\n\
+fmc-interval \n\
++ Same as default, but with intervals for models of integer functions.\n\
+\n\
+abs \n\
++ Use abstract MBQI algorithm (uses disjoint sets). \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_qcfWhenModeHelp = "\
+Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\
+\n\
+default \n\
++ Default, apply conflict finding at full effort.\n\
+\n\
+last-call \n\
++ Apply conflict finding at last call, after theory combination and \n\
+  and all theories report sat. \n\
+\n\
+std \n\
++ Apply conflict finding at standard effort.\n\
+\n\
+std-h \n\
++ Apply conflict finding at standard effort when heuristic says to. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_qcfModeHelp = "\
+Quantifier conflict find modes currently supported by the --quant-cf option:\n\
+\n\
+prop-eq \n\
++ Default, apply QCF algorithm to propagate equalities as well as conflicts. \n\
+\n\
+conflict \n\
++ Apply QCF algorithm to find conflicts only.\n\
+\n\
+partial \n\
++ Apply QCF algorithm to instantiate heuristically as well. \n\
+\n\
+mc \n\
++ Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_userPatModeHelp = "\
+User pattern modes currently supported by the --user-pat option:\n\
+\n\
+trust \n\
++ When provided, use only user-provided patterns for a quantified formula.\n\
+\n\
+use \n\
++ Use both user-provided and auto-generated patterns when patterns\n\
+  are provided for a quantified formula.\n\
+\n\
+resort \n\
++ Use user-provided patterns only after auto-generated patterns saturate.\n\
+\n\
+ignore \n\
++ Ignore user-provided patterns. \n\
+\n\
+interleave \n\
++ Alternate between use/resort. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_triggerSelModeHelp = "\
+Trigger selection modes currently supported by the --trigger-sel option:\n\
+\n\
+default \n\
++ Default, consider all subterms of quantified formulas for trigger selection.\n\
+\n\
+min \n\
++ Consider only minimal subterms that meet criteria for triggers.\n\
+\n\
+max \n\
++ Consider only maximal subterms that meet criteria for triggers. \n\
+\n\
+";
+const std::string SmtOptionsHandler::s_prenexQuantModeHelp = "\
+Prenex quantifiers modes currently supported by the --prenex-quant option:\n\
+\n\
+default \n\
++ Default, prenex all nested quantifiers except those with user patterns.\n\
+\n\
+all \n\
++ Prenex all nested quantifiers.\n\
+\n\
+none \n\
++ Do no prenex nested quantifiers. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_cegqiFairModeHelp = "\
+Modes for enforcing fairness for counterexample guided quantifier instantion, supported by --cegqi-fair:\n\
+\n\
+uf-dt-size \n\
++ Enforce fairness using an uninterpreted function for datatypes size.\n\
+\n\
+default | dt-size \n\
++ Default, enforce fairness using size theory operator.\n\
+\n\
+dt-height-bound \n\
++ Enforce fairness by height bound predicate.\n\
+\n\
+none \n\
++ Do not enforce fairness. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_termDbModeHelp = "\
+Modes for term database, supported by --term-db-mode:\n\
+\n\
+all  \n\
++ Quantifiers module considers all ground terms.\n\
+\n\
+relevant \n\
++ Quantifiers module considers only ground terms connected to current assertions. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_iteLiftQuantHelp = "\
+Modes for term database, supported by --ite-lift-quant:\n\
+\n\
+none  \n\
++ Do not lift if-then-else in quantified formulas.\n\
+\n\
+simple  \n\
++ Lift if-then-else in quantified formulas if results in smaller term size.\n\
+\n\
+all \n\
++ Lift if-then-else in quantified formulas. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_sygusInvTemplHelp = "\
+Template modes for sygus invariant synthesis, supported by --sygus-inv-templ:\n\
+\n\
+none  \n\
++ Synthesize invariant directly.\n\
+\n\
+pre  \n\
++ Synthesize invariant based on weakening of precondition .\n\
+\n\
+post \n\
++ Synthesize invariant based on strengthening of postcondition. \n\
+\n\
+";
+
+const std::string SmtOptionsHandler::s_macrosQuantHelp = "\
+Template modes for quantifiers macro expansion, supported by --macros-quant-mode:\n\
+\n\
+all \n\
++ Infer definitions for functions, including those containing quantified formulas.\n\
+\n\
+ground (default) \n\
++ Only infer ground definitions for functions.\n\
+\n\
+ground-uf \n\
++ Only infer ground definitions for functions that result in triggers for all free variables.\n\
+\n\
+";
+
+theory::quantifiers::InstWhenMode SmtOptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "pre-full") {
+    return theory::quantifiers::INST_WHEN_PRE_FULL;
+  } else if(optarg == "full") {
+    return theory::quantifiers::INST_WHEN_FULL;
+  } else if(optarg == "full-delay") {
+    return theory::quantifiers::INST_WHEN_FULL_DELAY;
+  } else if(optarg == "full-last-call") {
+    return theory::quantifiers::INST_WHEN_FULL_LAST_CALL;
+  } else if(optarg == "full-delay-last-call") {
+    return theory::quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL;
+  } else if(optarg == "last-call") {
+    return theory::quantifiers::INST_WHEN_LAST_CALL;
+  } else if(optarg == "help") {
+    puts(s_instWhenHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --inst-when: `") +
+                          optarg + "'.  Try --inst-when help.");
+  }
+}
+
+void SmtOptionsHandler::checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException)  {
+  if(mode == theory::quantifiers::INST_WHEN_PRE_FULL) {
+    throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
+  }
+}
+
+theory::quantifiers::LiteralMatchMode SmtOptionsHandler::stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "none") {
+    return theory::quantifiers::LITERAL_MATCH_NONE;
+  } else if(optarg ==  "predicate") {
+    return theory::quantifiers::LITERAL_MATCH_PREDICATE;
+  } else if(optarg ==  "equality") {
+    return theory::quantifiers::LITERAL_MATCH_EQUALITY;
+  } else if(optarg ==  "help") {
+    puts(s_literalMatchHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --literal-matching: `") +
+                          optarg + "'.  Try --literal-matching help.");
+  }
+}
+
+void SmtOptionsHandler::checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException) {
+  if(mode == theory::quantifiers::LITERAL_MATCH_EQUALITY) {
+    throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
+  }
+}
+
+theory::quantifiers::MbqiMode SmtOptionsHandler::stringToMbqiMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "gen-ev") {
+    return theory::quantifiers::MBQI_GEN_EVAL;
+  } else if(optarg == "none") {
+    return theory::quantifiers::MBQI_NONE;
+  } else if(optarg == "default" || optarg ==  "fmc") {
+    return theory::quantifiers::MBQI_FMC;
+  } else if(optarg == "fmc-interval") {
+    return theory::quantifiers::MBQI_FMC_INTERVAL;
+  } else if(optarg == "abs") {
+    return theory::quantifiers::MBQI_ABS;
+  } else if(optarg == "trust") {
+    return theory::quantifiers::MBQI_TRUST;
+  } else if(optarg == "help") {
+    puts(s_mbqiModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --mbqi: `") +
+                          optarg + "'.  Try --mbqi help.");
+  }
+}
+
+
+void SmtOptionsHandler::checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException) {}
+
+
+theory::quantifiers::QcfWhenMode SmtOptionsHandler::stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "default") {
+    return theory::quantifiers::QCF_WHEN_MODE_DEFAULT;
+  } else if(optarg ==  "last-call") {
+    return theory::quantifiers::QCF_WHEN_MODE_LAST_CALL;
+  } else if(optarg ==  "std") {
+    return theory::quantifiers::QCF_WHEN_MODE_STD;
+  } else if(optarg ==  "std-h") {
+    return theory::quantifiers::QCF_WHEN_MODE_STD_H;
+  } else if(optarg ==  "help") {
+    puts(s_qcfWhenModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --quant-cf-when: `") +
+                          optarg + "'.  Try --quant-cf-when help.");
+  }
+}
+
+theory::quantifiers::QcfMode SmtOptionsHandler::stringToQcfMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "conflict") {
+    return theory::quantifiers::QCF_CONFLICT_ONLY;
+  } else if(optarg ==  "default" || optarg == "prop-eq") {
+    return theory::quantifiers::QCF_PROP_EQ;
+  } else if(optarg == "partial") {
+    return theory::quantifiers::QCF_PARTIAL;
+  } else if(optarg == "mc" ) {
+    return theory::quantifiers::QCF_MC;
+  } else if(optarg ==  "help") {
+    puts(s_qcfModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --quant-cf-mode: `") +
+                          optarg + "'.  Try --quant-cf-mode help.");
+  }
+}
+
+theory::quantifiers::UserPatMode SmtOptionsHandler::stringToUserPatMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "use") {
+    return theory::quantifiers::USER_PAT_MODE_USE;
+  } else if(optarg ==  "default" || optarg == "trust") {
+    return theory::quantifiers::USER_PAT_MODE_TRUST;
+  } else if(optarg == "resort") {
+    return theory::quantifiers::USER_PAT_MODE_RESORT;
+  } else if(optarg == "ignore") {
+    return theory::quantifiers::USER_PAT_MODE_IGNORE;
+  } else if(optarg == "interleave") {
+    return theory::quantifiers::USER_PAT_MODE_INTERLEAVE;
+  } else if(optarg ==  "help") {
+    puts(s_userPatModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --user-pat: `") +
+                          optarg + "'.  Try --user-pat help.");
+  }
+}
+
+theory::quantifiers::TriggerSelMode SmtOptionsHandler::stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "default" || optarg == "all" ) {
+    return theory::quantifiers::TRIGGER_SEL_DEFAULT;
+  } else if(optarg == "min") {
+    return theory::quantifiers::TRIGGER_SEL_MIN;
+  } else if(optarg == "max") {
+    return theory::quantifiers::TRIGGER_SEL_MAX;
+  } else if(optarg ==  "help") {
+    puts(s_triggerSelModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --trigger-sel: `") +
+                          optarg + "'.  Try --trigger-sel help.");
+  }
+}
+
+
+theory::quantifiers::PrenexQuantMode SmtOptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "default" ) {
+    return theory::quantifiers::PRENEX_NO_USER_PAT;
+  } else if(optarg == "all") {
+    return theory::quantifiers::PRENEX_ALL;
+  } else if(optarg == "none") {
+    return theory::quantifiers::PRENEX_NONE;
+  } else if(optarg ==  "help") {
+    puts(s_prenexQuantModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --prenex-quant: `") +
+                          optarg + "'.  Try --prenex-quant help.");
+  }
+}
+
+theory::quantifiers::CegqiFairMode SmtOptionsHandler::stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "uf-dt-size" ) {
+    return theory::quantifiers::CEGQI_FAIR_UF_DT_SIZE;
+  } else if(optarg == "default" || optarg == "dt-size") {
+    return theory::quantifiers::CEGQI_FAIR_DT_SIZE;
+  } else if(optarg == "dt-height-bound" ){
+    return theory::quantifiers::CEGQI_FAIR_DT_HEIGHT_PRED;
+  } else if(optarg == "none") {
+    return theory::quantifiers::CEGQI_FAIR_NONE;
+  } else if(optarg ==  "help") {
+    puts(s_cegqiFairModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --cegqi-fair: `") +
+                          optarg + "'.  Try --cegqi-fair help.");
+  }
+}
+
+theory::quantifiers::TermDbMode SmtOptionsHandler::stringToTermDbMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "all" ) {
+    return theory::quantifiers::TERM_DB_ALL;
+  } else if(optarg == "relevant") {
+    return theory::quantifiers::TERM_DB_RELEVANT;
+  } else if(optarg ==  "help") {
+    puts(s_termDbModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --term-db-mode: `") +
+                          optarg + "'.  Try --term-db-mode help.");
+  }
+}
+
+theory::quantifiers::IteLiftQuantMode SmtOptionsHandler::stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "all" ) {
+    return theory::quantifiers::ITE_LIFT_QUANT_MODE_ALL;
+  } else if(optarg == "simple") {
+    return theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE;
+  } else if(optarg == "none") {
+    return theory::quantifiers::ITE_LIFT_QUANT_MODE_NONE;
+  } else if(optarg ==  "help") {
+    puts(s_iteLiftQuantHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --ite-lift-quant: `") +
+                          optarg + "'.  Try --ite-lift-quant help.");
+  }
+}
+
+theory::quantifiers::SygusInvTemplMode SmtOptionsHandler::stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "none" ) {
+    return theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE;
+  } else if(optarg == "pre") {
+    return theory::quantifiers::SYGUS_INV_TEMPL_MODE_PRE;
+  } else if(optarg == "post") {
+    return theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST;
+  } else if(optarg ==  "help") {
+    puts(s_sygusInvTemplHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --sygus-inv-templ: `") +
+                          optarg + "'.  Try --sygus-inv-templ help.");
+  }
+}
+
+theory::quantifiers::MacrosQuantMode SmtOptionsHandler::stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "all" ) {
+    return theory::quantifiers::MACROS_QUANT_MODE_ALL;
+  } else if(optarg == "ground") {
+    return theory::quantifiers::MACROS_QUANT_MODE_GROUND;
+  } else if(optarg == "ground-uf") {
+    return theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF;
+  } else if(optarg ==  "help") {
+    puts(s_macrosQuantHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --macros-quant-mode: `") +
+                          optarg + "'.  Try --macros-quant-mode help.");
+  }
+}
+
+
+
+// theory/bv/options_handlers.h
+void SmtOptionsHandler::abcEnabledBuild(std::string option, bool value) throw(OptionException) {
+#ifndef CVC4_USE_ABC
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_ABC */
+}
+
+void SmtOptionsHandler::abcEnabledBuild(std::string option, std::string value) throw(OptionException) {
+#ifndef CVC4_USE_ABC
+  if(!value.empty()) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_USE_ABC */
+}
+
+const std::string SmtOptionsHandler::s_bitblastingModeHelp = "\
+Bit-blasting modes currently supported by the --bitblast option:\n\
+\n\
+lazy (default)\n\
++ Separate boolean structure and term reasoning betwen the core\n\
+  SAT solver and the bv SAT solver\n\
+\n\
+eager\n\
++ Bitblast eagerly to bv SAT solver\n\
+";
+
+theory::bv::BitblastMode SmtOptionsHandler::stringToBitblastMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "lazy") {
+    if (!options::bitvectorPropagate.wasSetByUser()) {
+      options::bitvectorPropagate.set(true);
+    }
+    if (!options::bitvectorEqualitySolver.wasSetByUser()) {
+      options::bitvectorEqualitySolver.set(true);
+    }
+    if (!options::bitvectorEqualitySlicer.wasSetByUser()) {
+      if (options::incrementalSolving() ||
+          options::produceModels()) {
+        options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_OFF);
+      } else {
+        options::bitvectorEqualitySlicer.set(theory::bv::BITVECTOR_SLICER_AUTO);
+      }
+    }
+
+    if (!options::bitvectorInequalitySolver.wasSetByUser()) {
+      options::bitvectorInequalitySolver.set(true);
+    }
+    if (!options::bitvectorAlgebraicSolver.wasSetByUser()) {
+      options::bitvectorAlgebraicSolver.set(true);
+    }
+    return theory::bv::BITBLAST_MODE_LAZY;
+  } else if(optarg == "eager") {
+
+    if (options::incrementalSolving() &&
+        options::incrementalSolving.wasSetByUser()) {
+      throw OptionException(std::string("Eager bit-blasting does not currently support incremental mode. \n\
+                                         Try --bitblast=lazy"));
+    }
+    if (!options::bitvectorToBool.wasSetByUser()) {
+      options::bitvectorToBool.set(true);
+    }
+
+    if (!options::bvAbstraction.wasSetByUser() &&
+        !options::skolemizeArguments.wasSetByUser()) {
+      options::bvAbstraction.set(true);
+      options::skolemizeArguments.set(true);
+    }
+    return theory::bv::BITBLAST_MODE_EAGER;
+  } else if(optarg == "help") {
+    puts(s_bitblastingModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --bitblast: `") +
+                          optarg + "'.  Try --bitblast=help.");
+  }
+}
+
+const std::string SmtOptionsHandler::s_bvSlicerModeHelp = "\
+Bit-vector equality slicer modes supported by the --bv-eq-slicer option:\n\
+\n\
+auto (default)\n\
++ Turn slicer on if input has only equalities over core symbols\n\
+\n\
+on\n\
++ Turn slicer on\n\
+\n\
+off\n\
++ Turn slicer off\n\
+";
+
+theory::bv::BvSlicerMode SmtOptionsHandler::stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "auto") {
+    return theory::bv::BITVECTOR_SLICER_AUTO;
+  } else if(optarg == "on") {
+    return theory::bv::BITVECTOR_SLICER_ON;
+  } else if(optarg == "off") {
+    return theory::bv::BITVECTOR_SLICER_OFF;
+  } else if(optarg == "help") {
+    puts(s_bitblastingModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --bv-eq-slicer: `") +
+                          optarg + "'.  Try --bv-eq-slicer=help.");
+  }
+}
+
+void SmtOptionsHandler::setBitblastAig(std::string option, bool arg) throw(OptionException) {
+  if(arg) {
+    if(options::bitblastMode.wasSetByUser()) {
+      if(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER) {
+        throw OptionException("bitblast-aig must be used with eager bitblaster");
+      }
+    } else {
+      theory::bv::BitblastMode mode = stringToBitblastMode("", "eager");
+      options::bitblastMode.set(mode);
+    }
+    if(!options::bitvectorAigSimplifications.wasSetByUser()) {
+      options::bitvectorAigSimplifications.set("balance;drw");
+    }
+  }
+}
+
+
+// theory/booleans/options_handlers.h
+const std::string SmtOptionsHandler::s_booleanTermConversionModeHelp = "\
+Boolean term conversion modes currently supported by the\n\
+--boolean-term-conversion-mode option:\n\
+\n\
+bitvectors [default]\n\
++ Boolean terms are converted to bitvectors of size 1.\n\
+\n\
+datatypes\n\
++ Boolean terms are converted to enumerations in the Datatype theory.\n\
+\n\
+native\n\
++ Boolean terms are converted in a \"natural\" way depending on where they\n\
+  are used.  If in a datatype context, they are converted to an enumeration.\n\
+  Elsewhere, they are converted to a bitvector of size 1.\n\
+";
+
+theory::booleans::BooleanTermConversionMode SmtOptionsHandler::stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException){
+  if(optarg ==  "bitvectors") {
+    return theory::booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS;
+  } else if(optarg ==  "datatypes") {
+    return theory::booleans::BOOLEAN_TERM_CONVERT_TO_DATATYPES;
+  } else if(optarg ==  "native") {
+    return theory::booleans::BOOLEAN_TERM_CONVERT_NATIVE;
+  } else if(optarg ==  "help") {
+    puts(s_booleanTermConversionModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --boolean-term-conversion-mode: `") +
+                          optarg + "'.  Try --boolean-term-conversion-mode help.");
+  }
+}
+
+// theory/uf/options_handlers.h
+const std::string SmtOptionsHandler::s_ufssModeHelp = "\
+UF strong solver options currently supported by the --uf-ss option:\n\
+\n\
+full \n\
++ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\
+\n\
+no-minimal \n\
++ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\
+\n\
+none \n\
++ Do not use uf strong solver to shrink model sizes. \n\
+\n\
+";
+
+theory::uf::UfssMode SmtOptionsHandler::stringToUfssMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg ==  "default" || optarg == "full" ) {
+    return theory::uf::UF_SS_FULL;
+  } else if(optarg == "no-minimal") {
+    return theory::uf::UF_SS_NO_MINIMAL;
+  } else if(optarg == "none") {
+    return theory::uf::UF_SS_NONE;
+  } else if(optarg ==  "help") {
+    puts(s_ufssModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --uf-ss: `") +
+                          optarg + "'.  Try --uf-ss help.");
+  }
+}
+
+
+
+// theory/options_handlers.h
+const std::string SmtOptionsHandler::s_theoryOfModeHelp = "\
+TheoryOf modes currently supported by the --theoryof-mode option:\n\
+\n\
+type (default) \n\
++ type variables, constants and equalities by type\n\
+\n\
+term \n\
++ type variables as uninterpreted, equalities by the parametric theory\n\
+";
+
+theory::TheoryOfMode SmtOptionsHandler::stringToTheoryOfMode(std::string option, std::string optarg) {
+  if(optarg == "type") {
+    return theory::THEORY_OF_TYPE_BASED;
+  } else if(optarg == "term") {
+    return theory::THEORY_OF_TERM_BASED;
+  } else if(optarg == "help") {
+    puts(s_theoryOfModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --theoryof-mode: `") +
+                          optarg + "'.  Try --theoryof-mode help.");
+  }
+}
+
+void SmtOptionsHandler::useTheory(std::string option, std::string optarg) {
+  if(optarg == "help") {
+    puts(theory::useTheoryHelp);
+    exit(1);
+  }
+  if(theory::useTheoryValidate(optarg)) {
+    std::map<std::string, bool> m = options::theoryAlternates();
+    m[optarg] = true;
+    options::theoryAlternates.set(m);
+  } else {
+    throw OptionException(std::string("unknown option for ") + option + ": `" +
+                          optarg + "'.  Try --use-theory help.");
+  }
+}
+
+
+
+// printer/options_handlers.h
+const std::string SmtOptionsHandler::s_modelFormatHelp = "\
+Model format modes currently supported by the --model-format option:\n\
+\n\
+default \n\
++ Print model as expressions in the output language format.\n\
+\n\
+table\n\
++ Print functional expressions over finite domains in a table format.\n\
+";
+
+const std::string SmtOptionsHandler::s_instFormatHelp = "\
+Inst format modes currently supported by the --model-format option:\n\
+\n\
+default \n\
++ Print instantiations as a list in the output language format.\n\
+\n\
+szs\n\
++ Print instantiations as SZS compliant proof.\n\
+";
+
+ModelFormatMode SmtOptionsHandler::stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "default") {
+    return MODEL_FORMAT_MODE_DEFAULT;
+  } else if(optarg == "table") {
+    return MODEL_FORMAT_MODE_TABLE;
+  } else if(optarg == "help") {
+    puts(s_modelFormatHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --model-format: `") +
+                          optarg + "'.  Try --model-format help.");
+  }
+}
+
+InstFormatMode SmtOptionsHandler::stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "default") {
+    return INST_FORMAT_MODE_DEFAULT;
+  } else if(optarg == "szs") {
+    return INST_FORMAT_MODE_SZS;
+  } else if(optarg == "help") {
+    puts(s_instFormatHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --inst-format: `") +
+                          optarg + "'.  Try --inst-format help.");
+  }
+}
+
+
+
+// decision/options_handlers.h
+const std::string SmtOptionsHandler::s_decisionModeHelp = "\
+Decision modes currently supported by the --decision option:\n\
+\n\
+internal (default)\n\
++ Use the internal decision heuristics of the SAT solver\n\
+\n\
+justification\n\
++ An ATGP-inspired justification heuristic\n\
+\n\
+justification-stoponly\n\
++ Use the justification heuristic only to stop early, not for decisions\n\
+";
+
+decision::DecisionMode SmtOptionsHandler::stringToDecisionMode(std::string option, std::string optarg) throw(OptionException) {
+  options::decisionStopOnly.set(false);
+
+  if(optarg == "internal") {
+    return decision::DECISION_STRATEGY_INTERNAL;
+  } else if(optarg == "justification") {
+    return decision::DECISION_STRATEGY_JUSTIFICATION;
+  } else if(optarg == "justification-stoponly") {
+    options::decisionStopOnly.set(true);
+    return decision::DECISION_STRATEGY_JUSTIFICATION;
+  } else if(optarg == "help") {
+    puts(s_decisionModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --decision: `") +
+                          optarg + "'.  Try --decision help.");
+  }
+}
+
+decision::DecisionWeightInternal SmtOptionsHandler::stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "off")
+    return decision::DECISION_WEIGHT_INTERNAL_OFF;
+  else if(optarg == "max")
+    return decision::DECISION_WEIGHT_INTERNAL_MAX;
+  else if(optarg == "sum")
+    return decision::DECISION_WEIGHT_INTERNAL_SUM;
+  else if(optarg == "usr1")
+    return decision::DECISION_WEIGHT_INTERNAL_USR1;
+  else
+    throw OptionException(std::string("--decision-weight-internal must be off, max or sum."));
+}
+
+
+
+// smt/options_handlers.h
+const std::string SmtOptionsHandler::SmtOptionsHandler::s_dumpHelp = "\
+Dump modes currently supported by the --dump option:\n\
+\n\
+benchmark\n\
++ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\
+  does not include any declarations or assertions.  Implied by all following\n\
+  modes.\n\
+\n\
+declarations\n\
++ Dump user declarations.  Implied by all following modes.\n\
+\n\
+skolems\n\
++ Dump internally-created skolem variable declarations.  These can\n\
+  arise from preprocessing simplifications, existential elimination,\n\
+  and a number of other things.  Implied by all following modes.\n\
+\n\
+assertions\n\
++ Output the assertions after preprocessing and before clausification.\n\
+  Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
+  where PASS is one of the preprocessing passes: definition-expansion\n\
+  boolean-terms constrain-subtypes substitution strings-pp skolem-quant\n\
+  simplify static-learning ite-removal repeat-simplify\n\
+  rewrite-apply-to-const theory-preprocessing.\n\
+  PASS can also be the special value \"everything\", in which case the\n\
+  assertions are printed before any preprocessing (with\n\
+  \"assertions:pre-everything\") or after all preprocessing completes\n\
+  (with \"assertions:post-everything\").\n\
+\n\
+clauses\n\
++ Do all the preprocessing outlined above, and dump the CNF-converted\n\
+  output\n\
+\n\
+state\n\
++ Dump all contextual assertions (e.g., SAT decisions, propagations..).\n\
+  Implied by all \"stateful\" modes below and conflicts with all\n\
+  non-stateful modes below.\n\
+\n\
+t-conflicts [non-stateful]\n\
++ Output correctness queries for all theory conflicts\n\
+\n\
+missed-t-conflicts [stateful]\n\
++ Output completeness queries for theory conflicts\n\
+\n\
+t-propagations [stateful]\n\
++ Output correctness queries for all theory propagations\n\
+\n\
+missed-t-propagations [stateful]\n\
++ Output completeness queries for theory propagations (LARGE and EXPENSIVE)\n\
+\n\
+t-lemmas [non-stateful]\n\
++ Output correctness queries for all theory lemmas\n\
+\n\
+t-explanations [non-stateful]\n\
++ Output correctness queries for all theory explanations\n\
+\n\
+bv-rewrites [non-stateful]\n\
++ Output correctness queries for all bitvector rewrites\n\
+\n\
+bv-abstraction [non-stateful]\n\
++ Output correctness queries for all bv abstraction \n\
+\n\
+bv-algebraic [non-stateful]\n\
++ Output correctness queries for bv algebraic solver. \n\
+\n\
+theory::fullcheck [non-stateful]\n                                      \
++ Output completeness queries for all full-check effort-level theory checks\n\
+\n\
+Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
+one from the assertions category (either assertions or clauses), and\n\
+perhaps one or more stateful or non-stateful modes for checking correctness\n\
+and completeness of decision procedure implementations.  Stateful modes dump\n\
+the contextual assertions made by the core solver (all decisions and\n\
+propagations as assertions; that affects the validity of the resulting\n\
+correctness and completeness queries, so of course stateful and non-stateful\n\
+modes cannot be mixed in the same run.\n\
+\n\
+The --output-language option controls the language used for dumping, and\n\
+this allows you to connect CVC4 to another solver implementation via a UNIX\n\
+pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
+to a file.\n\
+";
+
+const std::string SmtOptionsHandler::s_simplificationHelp = "\
+Simplification modes currently supported by the --simplification option:\n\
+\n\
+batch (default) \n\
++ save up all ASSERTions; run nonclausal simplification and clausal\n\
+  (MiniSat) propagation for all of them only after reaching a querying command\n\
+  (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
+\n\
+none\n\
++ do not perform nonclausal simplification\n\
+";
+
+void SmtOptionsHandler::dumpMode(std::string option, std::string optarg) {
+#ifdef CVC4_DUMPING
+  char* optargPtr = strdup(optarg.c_str());
+  char* tokstr = optargPtr;
+  char* toksave;
+  while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
+    tokstr = NULL;
+    if(!strcmp(optargPtr, "benchmark")) {
+    } else if(!strcmp(optargPtr, "declarations")) {
+    } else if(!strcmp(optargPtr, "assertions")) {
+      Dump.on("assertions:post-everything");
+    } else if(!strncmp(optargPtr, "assertions:", 11)) {
+      const char* p = optargPtr + 11;
+      if(!strncmp(p, "pre-", 4)) {
+        p += 4;
+      } else if(!strncmp(p, "post-", 5)) {
+        p += 5;
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      if(!strcmp(p, "everything")) {
+      } else if(!strcmp(p, "definition-expansion")) {
+      } else if(!strcmp(p, "boolean-terms")) {
+      } else if(!strcmp(p, "constrain-subtypes")) {
+      } else if(!strcmp(p, "substitution")) {
+      } else if(!strcmp(p, "strings-pp")) {
+      } else if(!strcmp(p, "skolem-quant")) {
+      } else if(!strcmp(p, "simplify")) {
+      } else if(!strcmp(p, "static-learning")) {
+      } else if(!strcmp(p, "ite-removal")) {
+      } else if(!strcmp(p, "repeat-simplify")) {
+      } else if(!strcmp(p, "rewrite-apply-to-const")) {
+      } else if(!strcmp(p, "theory-preprocessing")) {
+      } else if(!strcmp(p, "nonclausal")) {
+      } else if(!strcmp(p, "theorypp")) {
+      } else if(!strcmp(p, "itesimp")) {
+      } else if(!strcmp(p, "unconstrained")) {
+      } else if(!strcmp(p, "repeatsimp")) {
+      } else {
+        throw OptionException(std::string("don't know how to dump `") +
+                              optargPtr + "'.  Please consult --dump help.");
+      }
+      Dump.on("assertions");
+    } else if(!strcmp(optargPtr, "skolems")) {
+    } else if(!strcmp(optargPtr, "clauses")) {
+    } else if(!strcmp(optargPtr, "t-conflicts") ||
+              !strcmp(optargPtr, "t-lemmas") ||
+              !strcmp(optargPtr, "t-explanations") ||
+              !strcmp(optargPtr, "bv-rewrites") ||
+              !strcmp(optargPtr, "theory::fullcheck")) {
+      // These are "non-state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is dumped, it will interfere with the validity
+      // of these generated queries.
+      if(Dump.isOn("state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("no-permit-state");
+      }
+    } else if(!strcmp(optargPtr, "state") ||
+              !strcmp(optargPtr, "missed-t-conflicts") ||
+              !strcmp(optargPtr, "t-propagations") ||
+              !strcmp(optargPtr, "missed-t-propagations")) {
+      // These are "state-dumping" modes.  If state (SAT decisions,
+      // propagations, etc.) is not dumped, it will interfere with the
+      // validity of these generated queries.
+      if(Dump.isOn("no-permit-state")) {
+        throw OptionException(std::string("dump option `") + optargPtr +
+                              "' conflicts with a previous, "
+                              "non-state-dumping dump option.  You cannot "
+                              "mix stateful and non-stateful dumping modes; "
+                              "see --dump help.");
+      } else {
+        Dump.on("state");
+      }
+    } else if(!strcmp(optargPtr, "help")) {
+      puts(s_dumpHelp.c_str());
+      exit(1);
+    } else if(!strcmp(optargPtr, "bv-abstraction")) {
+      Dump.on("bv-abstraction");
+    } else if(!strcmp(optargPtr, "bv-algebraic")) {
+      Dump.on("bv-algebraic");
+    } else {
+      throw OptionException(std::string("unknown option for --dump: `") +
+                            optargPtr + "'.  Try --dump help.");
+    }
+
+    Dump.on(optargPtr);
+    Dump.on("benchmark");
+    if(strcmp(optargPtr, "benchmark")) {
+      Dump.on("declarations");
+      if(strcmp(optargPtr, "declarations")) {
+        Dump.on("skolems");
+      }
+    }
+  }
+  free(optargPtr);
+#else /* CVC4_DUMPING */
+  throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+LogicInfo* SmtOptionsHandler::stringToLogicInfo(std::string option, std::string optarg) throw(OptionException) {
+  try {
+#warning "TODO: Fix the blatant memory leak here."
+    LogicInfo* logic = new LogicInfo(optarg);
+    if(d_smtEngine != NULL) {
+      d_smtEngine->setLogic(*logic);
+    }
+    return logic;
+  } catch(IllegalArgumentException& e) {
+    throw OptionException(std::string("invalid logic specification for --force-logic: `") +
+                          optarg + "':\n" + e.what());
+  }
+}
+
+SimplificationMode SmtOptionsHandler::stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "batch") {
+    return SIMPLIFICATION_MODE_BATCH;
+  } else if(optarg == "none") {
+    return SIMPLIFICATION_MODE_NONE;
+  } else if(optarg == "help") {
+    puts(s_simplificationHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --simplification: `") +
+                          optarg + "'.  Try --simplification help.");
+  }
+}
+
+
+void SmtOptionsHandler::beforeSearch(std::string option, bool value) throw(ModalException) {
+  SmtEngine::beforeSearch(d_smtEngine, option);
+}
+
+void SmtOptionsHandler::setProduceAssertions(std::string option, bool value) throw() {
+  options::produceAssertions.set(value);
+  options::interactiveMode.set(value);
+}
+
+
+void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw(OptionException) {
+#if !(IS_PROOFS_BUILD)
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires a proofs-enabled build of CVC4; this binary was not built with proof support";
+    throw OptionException(ss.str());
+  }
+#endif /* IS_PROOFS_BUILD */
+}
+
+
+// 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); \
+  }
+
+void SmtOptionsHandler::dumpToFile(std::string option, std::string optarg) {
+#ifdef CVC4_DUMPING
+  std::ostream* outStream = NULL;
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --dump-to"));
+  } else if(optarg == "-") {
+    outStream = &DumpOutC::dump_cout;
+  } else if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
+  } 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 dump-to file: `" << optarg << "': " << __cvc4_errno_failreason();
+      throw OptionException(ss.str());
+    }
+  }
+  __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 */
+}
+
+void SmtOptionsHandler::setRegularOutputChannel(std::string option, std::string optarg) {
+  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 if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
+  } 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 regular-output-channel file: `" << optarg << "': " << __cvc4_errno_failreason();
+      throw OptionException(ss.str());
+    }
+  }
+  __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(*options::err(), options::err.set(outStream));
+}
+
+void SmtOptionsHandler::setDiagnosticOutputChannel(std::string option, std::string optarg) {
+  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 if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
+  } 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
+
+
+
+std::string SmtOptionsHandler::checkReplayFilename(std::string option, std::string optarg) {
+#ifdef CVC4_REPLAY
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --replay"));
+  } else {
+    return optarg;
+  }
+#else /* CVC4_REPLAY */
+  throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+std::ostream* SmtOptionsHandler::checkReplayLogFilename(std::string option, std::string optarg) {
+#ifdef CVC4_REPLAY
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --replay-log"));
+  } else if(optarg == "-") {
+    return &std::cout;
+  } else if(!options::filesystemAccess()) {
+    throw OptionException(std::string("Filesystem access not permitted"));
+  } else {
+    errno = 0;
+    std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(replayLog == NULL || !*replayLog) {
+      std::stringstream ss;
+      ss << "Cannot open replay-log file: `" << optarg << "': " << __cvc4_errno_failreason();
+      throw OptionException(ss.str());
+    }
+    return replayLog;
+  }
+#else /* CVC4_REPLAY */
+  throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+void SmtOptionsHandler::statsEnabledBuild(std::string option, bool value) throw(OptionException) {
+#ifndef CVC4_STATISTICS_ON
+  if(value) {
+    std::stringstream ss;
+    ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
+    throw OptionException(ss.str());
+  }
+#endif /* CVC4_STATISTICS_ON */
+}
+
+unsigned long SmtOptionsHandler::tlimitHandler(std::string option, std::string optarg) throw(OptionException)  {
+  unsigned long ms;
+  std::istringstream convert(optarg);
+  if (!(convert >> ms)) {
+    throw OptionException("option `"+option+"` requires a number as an argument");
+  }
+
+  // make sure the resource is set if the option is updated
+  // if the smt engine is null the resource will be set in the
+  if (d_smtEngine != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager();
+    rm->setTimeLimit(ms, true);
+  }
+  return ms;
+}
+
+unsigned long SmtOptionsHandler::tlimitPerHandler(std::string option, std::string optarg) throw(OptionException) {
+  unsigned long ms;
+
+  std::istringstream convert(optarg);
+  if (!(convert >> ms)) {
+    throw OptionException("option `"+option+"` requires a number as an argument");
+  }
+
+  if (d_smtEngine != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager();
+    rm->setTimeLimit(ms, false);
+  }
+  return ms;
+}
+
+unsigned long SmtOptionsHandler::rlimitHandler(std::string option, std::string optarg) throw(OptionException) {
+  unsigned long ms;
+
+  std::istringstream convert(optarg);
+  if (!(convert >> ms)) {
+    throw OptionException("option `"+option+"` requires a number as an argument");
+  }
+
+  if (d_smtEngine != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager();
+    rm->setResourceLimit(ms, true);
+  }
+  return ms;
+}
+
+unsigned long SmtOptionsHandler::rlimitPerHandler(std::string option, std::string optarg) throw(OptionException) {
+  unsigned long ms;
+
+  std::istringstream convert(optarg);
+  if (!(convert >> ms)) {
+    throw OptionException("option `"+option+"` requires a number as an argument");
+  }
+
+  // TODO: Remove check?
+  if (d_smtEngine != NULL) {
+    ResourceManager* rm = NodeManager::fromExprManager(d_smtEngine->getExprManager())->getResourceManager();
+    rm->setResourceLimit(ms, false);
+  }
+  return ms;
+}
+
+
+
+// expr/options_handlers.h
+void SmtOptionsHandler::setDefaultExprDepth(std::string option, int depth) {
+  if(depth < -1) {
+    throw OptionException("--default-expr-depth requires a positive argument, or -1.");
+  }
+
+  Debug.getStream() << Expr::setdepth(depth);
+  Trace.getStream() << Expr::setdepth(depth);
+  Notice.getStream() << Expr::setdepth(depth);
+  Chat.getStream() << Expr::setdepth(depth);
+  Message.getStream() << Expr::setdepth(depth);
+  Warning.getStream() << Expr::setdepth(depth);
+  // intentionally exclude Dump stream from this list
+}
+
+void SmtOptionsHandler::setDefaultDagThresh(std::string option, int dag) {
+  if(dag < 0) {
+    throw OptionException("--default-dag-thresh requires a nonnegative argument.");
+  }
+
+  Debug.getStream() << Expr::dag(dag);
+  Trace.getStream() << Expr::dag(dag);
+  Notice.getStream() << Expr::dag(dag);
+  Chat.getStream() << Expr::dag(dag);
+  Message.getStream() << Expr::dag(dag);
+  Warning.getStream() << Expr::dag(dag);
+  Dump.getStream() << Expr::dag(dag);
+}
+
+void SmtOptionsHandler::setPrintExprTypes(std::string option) {
+  Debug.getStream() << Expr::printtypes(true);
+  Trace.getStream() << Expr::printtypes(true);
+  Notice.getStream() << Expr::printtypes(true);
+  Chat.getStream() << Expr::printtypes(true);
+  Message.getStream() << Expr::printtypes(true);
+  Warning.getStream() << Expr::printtypes(true);
+  // intentionally exclude Dump stream from this list
+}
+
+
+// main/options_handlers.h
+void SmtOptionsHandler::showConfiguration(std::string option) {
+  fputs(Configuration::about().c_str(), stdout);
+  printf("\n");
+  printf("version    : %s\n", Configuration::getVersionString().c_str());
+  if(Configuration::isGitBuild()) {
+    const char* branchName = Configuration::getGitBranchName();
+    if(*branchName == '\0') {
+      branchName = "-";
+    }
+    printf("scm        : git [%s %s%s]\n",
+           branchName,
+           std::string(Configuration::getGitCommit()).substr(0, 8).c_str(),
+           Configuration::hasGitModifications() ?
+             " (with modifications)" : "");
+  } else if(Configuration::isSubversionBuild()) {
+    printf("scm        : svn [%s r%u%s]\n",
+           Configuration::getSubversionBranchName(),
+           Configuration::getSubversionRevision(),
+           Configuration::hasSubversionModifications() ?
+             " (with modifications)" : "");
+  } else {
+    printf("scm        : no\n");
+  }
+  printf("\n");
+  printf("library    : %u.%u.%u\n",
+         Configuration::getVersionMajor(),
+         Configuration::getVersionMinor(),
+         Configuration::getVersionRelease());
+  printf("\n");
+  printf("debug code : %s\n", Configuration::isDebugBuild() ? "yes" : "no");
+  printf("statistics : %s\n", Configuration::isStatisticsBuild() ? "yes" : "no");
+  printf("replay     : %s\n", Configuration::isReplayBuild() ? "yes" : "no");
+  printf("tracing    : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
+  printf("dumping    : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
+  printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
+  printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
+  printf("proof      : %s\n", Configuration::isProofBuild() ? "yes" : "no");
+  printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
+  printf("profiling  : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
+  printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
+  printf("\n");
+  printf("cudd       : %s\n", Configuration::isBuiltWithCudd() ? "yes" : "no");
+  printf("cln        : %s\n", Configuration::isBuiltWithCln() ? "yes" : "no");
+  printf("gmp        : %s\n", Configuration::isBuiltWithGmp() ? "yes" : "no");
+  printf("glpk       : %s\n", Configuration::isBuiltWithGlpk() ? "yes" : "no");
+  printf("abc        : %s\n", Configuration::isBuiltWithAbc() ? "yes" : "no");
+  printf("readline   : %s\n", Configuration::isBuiltWithReadline() ? "yes" : "no");
+  printf("tls        : %s\n", Configuration::isBuiltWithTlsSupport() ? "yes" : "no");
+  exit(0);
+}
+
+void SmtOptionsHandler::showDebugTags(std::string option) {
+  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
+    printf("available tags:");
+    unsigned ntags = Configuration::getNumDebugTags();
+    char const* const* tags = Configuration::getDebugTags();
+    for(unsigned i = 0; i < ntags; ++ i) {
+      printf(" %s", tags[i]);
+    }
+    printf("\n");
+  } 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");
+  }
+  exit(0);
+}
+
+void SmtOptionsHandler::showTraceTags(std::string option) {
+  if(Configuration::isTracingBuild()) {
+    printf("available tags:");
+    unsigned ntags = Configuration::getNumTraceTags();
+    char const* const* tags = Configuration::getTraceTags();
+    for (unsigned i = 0; i < ntags; ++ i) {
+      printf(" %s", tags[i]);
+    }
+    printf("\n");
+  } else {
+    throw OptionException("trace tags not available in non-tracing build");
+  }
+  exit(0);
+}
+
+void SmtOptionsHandler::threadN(std::string option) {
+  throw OptionException(option + " is not a real option by itself.  Use e.g. --thread0=\"--random-seed=10 --random-freq=0.02\" --thread1=\"--random-seed=20 --random-freq=0.05\"");
+}
+
+
+
+/* options/base_options_handlers.h */
+void SmtOptionsHandler::setVerbosity(std::string option, int value) throw(OptionException) {
+  if(Configuration::isMuzzledBuild()) {
+    DebugChannel.setStream(CVC4::null_os);
+    TraceChannel.setStream(CVC4::null_os);
+    NoticeChannel.setStream(CVC4::null_os);
+    ChatChannel.setStream(CVC4::null_os);
+    MessageChannel.setStream(CVC4::null_os);
+    WarningChannel.setStream(CVC4::null_os);
+  } else {
+    if(value < 2) {
+      ChatChannel.setStream(CVC4::null_os);
+    } else {
+      ChatChannel.setStream(std::cout);
+    }
+    if(value < 1) {
+      NoticeChannel.setStream(CVC4::null_os);
+    } else {
+      NoticeChannel.setStream(std::cout);
+    }
+    if(value < 0) {
+      MessageChannel.setStream(CVC4::null_os);
+      WarningChannel.setStream(CVC4::null_os);
+    } else {
+      MessageChannel.setStream(std::cout);
+      WarningChannel.setStream(std::cerr);
+    }
+  }
+}
+
+void SmtOptionsHandler::increaseVerbosity(std::string option) {
+  options::verbosity.set(options::verbosity() + 1);
+  setVerbosity(option, options::verbosity());
+}
+
+void SmtOptionsHandler::decreaseVerbosity(std::string option) {
+  options::verbosity.set(options::verbosity() - 1);
+  setVerbosity(option, options::verbosity());
+}
+
+OutputLanguage SmtOptionsHandler::stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "help") {
+    options::languageHelp.set(true);
+    return language::output::LANG_AUTO;
+  }
+
+  try {
+    return language::toOutputLanguage(optarg);
+  } catch(OptionException& oe) {
+    throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --output-language help");
+  }
+
+  Unreachable();
+}
+
+InputLanguage SmtOptionsHandler::stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) {
+  if(optarg == "help") {
+    options::languageHelp.set(true);
+    return language::input::LANG_AUTO;
+  }
+
+  try {
+    return language::toInputLanguage(optarg);
+  } catch(OptionException& oe) {
+    throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --language help");
+  }
+
+  Unreachable();
+}
+
+void SmtOptionsHandler::addTraceTag(std::string option, std::string optarg) {
+  if(Configuration::isTracingBuild()) {
+    if(!Configuration::isTraceTag(optarg.c_str())) {
+
+      if(optarg == "help") {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumTraceTags();
+        char const* const* tags = Configuration::getTraceTags();
+        for(unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
+        }
+        printf("\n");
+        exit(0);
+      }
+
+      throw OptionException(std::string("trace tag ") + optarg +
+                            std::string(" not available.") +
+                            suggestTags(Configuration::getTraceTags(), optarg) );
+    }
+  } else {
+    throw OptionException("trace tags not available in non-tracing builds");
+  }
+  Trace.on(optarg);
+}
+
+void SmtOptionsHandler::addDebugTag(std::string option, std::string optarg) {
+  if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
+    if(!Configuration::isDebugTag(optarg.c_str()) &&
+       !Configuration::isTraceTag(optarg.c_str())) {
+
+      if(optarg == "help") {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumDebugTags();
+        char const* const* tags = Configuration::getDebugTags();
+        for(unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
+        }
+        printf("\n");
+        exit(0);
+      }
+
+      throw OptionException(std::string("debug tag ") + optarg +
+                            std::string(" not available.") +
+                            suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) );
+    }
+  } 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);
+}
+
+void SmtOptionsHandler::setPrintSuccess(std::string option, bool value) {
+  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);
+}
+
+
+std::string SmtOptionsHandler::suggestTags(char const* const* validTags, std::string inputTag,
+                                           char const* const* additionalTags)
+{
+  DidYouMean didYouMean;
+
+  const char* opt;
+  for(size_t i = 0; (opt = validTags[i]) != NULL; ++i) {
+    didYouMean.addWord(validTags[i]);
+  }
+  if(additionalTags != NULL) {
+    for(size_t i = 0; (opt = additionalTags[i]) != NULL; ++i) {
+      didYouMean.addWord(additionalTags[i]);
+    }
+  }
+
+  return  didYouMean.getMatchAsString(inputTag);
+}
+
+std::string SmtOptionsHandler::__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 */
+}
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/smt_options_handler.h b/src/smt/smt_options_handler.h
new file mode 100644
index 000000000..c4d27a722
--- /dev/null
+++ b/src/smt/smt_options_handler.h
@@ -0,0 +1,198 @@
+/*********************                                                        */
+/*! \file options_handler_interface.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Interface for custom handlers and predicates options.
+ **
+ ** Interface for custom handlers and predicates options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__SMT__SMT_OPTIONS_HANDLER_H
+#define __CVC4__SMT__SMT_OPTIONS_HANDLER_H
+
+#include <ostream>
+#include <string>
+
+#include "base/modal_exception.h"
+#include "options/arith_heuristic_pivot_rule.h"
+#include "options/arith_propagation_mode.h"
+#include "options/arith_unate_lemma_mode.h"
+#include "options/boolean_term_conversion_mode.h"
+#include "options/bv_bitblast_mode.h"
+#include "options/decision_mode.h"
+#include "options/language.h"
+#include "options/option_exception.h"
+#include "options/options_handler_interface.h"
+#include "options/printer_modes.h"
+#include "options/quantifiers_modes.h"
+#include "options/simplification_mode.h"
+#include "options/theoryof_mode.h"
+#include "options/ufss_mode.h"
+#include "smt/smt_engine.h"
+#include "theory/logic_info.h"
+
+namespace CVC4 {
+namespace smt {
+
+class CVC4_PUBLIC SmtOptionsHandler : public options::OptionsHandler {
+public:
+  SmtOptionsHandler(SmtEngine* smt);
+  ~SmtOptionsHandler();
+
+  // TODO
+  // theory/arith/options_handlers.h
+  // theory/quantifiers/options_handlers.h
+  // theory/bv/options_handlers.h
+  // theory/booleans/options_handlers.h
+  // theory/uf/options_handlers.h
+  // theory/options_handlers.h
+  // printer/options_handlers.h
+  // decision/options_handlers.h
+  // smt/options_handlers.h
+  // expr/options_handlers.h
+  // main/options_handlers.h
+  // options/base_options_handlers.h
+
+  // theory/arith/options_handlers.h
+  virtual ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg) throw(OptionException);
+  virtual ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg) throw(OptionException);
+  virtual ErrorSelectionRule stringToErrorSelectionRule(std::string option, std::string optarg) throw(OptionException);
+
+  // theory/quantifiers/options_handlers.h
+  virtual theory::quantifiers::InstWhenMode stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException);
+  virtual void checkInstWhenMode(std::string option, theory::quantifiers::InstWhenMode mode) throw(OptionException);
+  virtual theory::quantifiers::LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg) throw(OptionException);
+  virtual void checkLiteralMatchMode(std::string option, theory::quantifiers::LiteralMatchMode mode) throw(OptionException);
+  virtual theory::quantifiers::MbqiMode stringToMbqiMode(std::string option, std::string optarg) throw(OptionException);
+  virtual void checkMbqiMode(std::string option, theory::quantifiers::MbqiMode mode) throw(OptionException);
+  virtual theory::quantifiers::QcfWhenMode stringToQcfWhenMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::QcfMode stringToQcfMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::UserPatMode stringToUserPatMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::TriggerSelMode stringToTriggerSelMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::PrenexQuantMode stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::CegqiFairMode stringToCegqiFairMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::TermDbMode stringToTermDbMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::IteLiftQuantMode stringToIteLiftQuantMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::SygusInvTemplMode stringToSygusInvTemplMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::quantifiers::MacrosQuantMode stringToMacrosQuantMode(std::string option, std::string optarg) throw(OptionException);
+
+  // theory/bv/options_handlers.h
+  virtual void abcEnabledBuild(std::string option, bool value) throw(OptionException);
+  virtual void abcEnabledBuild(std::string option, std::string value) throw(OptionException);
+  virtual theory::bv::BitblastMode stringToBitblastMode(std::string option, std::string optarg) throw(OptionException);
+  virtual theory::bv::BvSlicerMode stringToBvSlicerMode(std::string option, std::string optarg) throw(OptionException);
+  virtual void setBitblastAig(std::string option, bool arg) throw(OptionException);
+
+
+  // theory/booleans/options_handlers.h
+  virtual theory::booleans::BooleanTermConversionMode stringToBooleanTermConversionMode(std::string option, std::string optarg) throw(OptionException);
+
+  // theory/uf/options_handlers.h
+  virtual theory::uf::UfssMode stringToUfssMode(std::string option, std::string optarg) throw(OptionException);
+
+  // theory/options_handlers.h
+  virtual theory::TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg);
+  virtual void useTheory(std::string option, std::string optarg);
+
+
+  // printer/options_handlers.h
+  virtual ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg) throw(OptionException);
+  virtual InstFormatMode stringToInstFormatMode(std::string option, std::string optarg) throw(OptionException);
+
+  // decision/options_handlers.h
+  virtual decision::DecisionMode stringToDecisionMode(std::string option, std::string optarg) throw(OptionException);
+  virtual decision::DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg) throw(OptionException);
+
+
+  // smt/options_handlers.h
+  virtual void dumpMode(std::string option, std::string optarg);
+  virtual LogicInfo* stringToLogicInfo(std::string option, std::string optarg) throw(OptionException);
+  virtual SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
+  virtual void beforeSearch(std::string option, bool value) throw(ModalException);
+  virtual void setProduceAssertions(std::string option, bool value) throw();
+  virtual void proofEnabledBuild(std::string option, bool value) throw(OptionException);
+  virtual void dumpToFile(std::string option, std::string optarg);
+  virtual void setRegularOutputChannel(std::string option, std::string optarg);
+  virtual void setDiagnosticOutputChannel(std::string option, std::string optarg);
+  virtual std::string checkReplayFilename(std::string option, std::string optarg);
+  virtual std::ostream* checkReplayLogFilename(std::string option, std::string optarg);
+  virtual void statsEnabledBuild(std::string option, bool value) throw(OptionException);
+  virtual unsigned long tlimitHandler(std::string option, std::string optarg) throw(OptionException);
+  virtual unsigned long tlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
+  virtual unsigned long rlimitHandler(std::string option, std::string optarg) throw(OptionException);
+  virtual unsigned long rlimitPerHandler(std::string option, std::string optarg) throw(OptionException);
+
+  /* expr/options_handlers.h */
+  virtual void setDefaultExprDepth(std::string option, int depth);
+  virtual void setDefaultDagThresh(std::string option, int dag);
+  virtual void setPrintExprTypes(std::string option);
+
+  /* main/options_handlers.h */
+  virtual void showConfiguration(std::string option);
+  virtual void showDebugTags(std::string option);
+  virtual void showTraceTags(std::string option);
+  virtual void threadN(std::string option);
+
+  /* options/base_options_handlers.h */
+  virtual void setVerbosity(std::string option, int value) throw(OptionException);
+  virtual void increaseVerbosity(std::string option);
+  virtual void decreaseVerbosity(std::string option);
+  virtual OutputLanguage stringToOutputLanguage(std::string option, std::string optarg) throw(OptionException);
+  virtual InputLanguage stringToInputLanguage(std::string option, std::string optarg) throw(OptionException) ;
+  virtual void addTraceTag(std::string option, std::string optarg);
+  virtual void addDebugTag(std::string option, std::string optarg);
+  virtual void setPrintSuccess(std::string option, bool value);
+
+private:
+  SmtEngine* d_smtEngine;
+
+  /* Helper utilities */
+  static std::string suggestTags(char const* const* validTags, std::string inputTag,
+                                 char const* const* additionalTags = NULL);
+  static std::string __cvc4_errno_failreason();
+
+  /* Help strings */
+  static const std::string s_bitblastingModeHelp;
+  static const std::string s_booleanTermConversionModeHelp;
+  static const std::string s_bvSlicerModeHelp;
+  static const std::string s_cegqiFairModeHelp;
+  static const std::string s_decisionModeHelp;
+  static const std::string s_dumpHelp;
+  static const std::string s_instFormatHelp ;
+  static const std::string s_instWhenHelp;
+  static const std::string s_iteLiftQuantHelp;
+  static const std::string s_literalMatchHelp;
+  static const std::string s_macrosQuantHelp;
+  static const std::string s_mbqiModeHelp;
+  static const std::string s_modelFormatHelp;
+  static const std::string s_prenexQuantModeHelp;
+  static const std::string s_qcfModeHelp;
+  static const std::string s_qcfWhenModeHelp;
+  static const std::string s_simplificationHelp;
+  static const std::string s_sygusInvTemplHelp;
+  static const std::string s_termDbModeHelp;
+  static const std::string s_theoryOfModeHelp;
+  static const std::string s_triggerSelModeHelp;
+  static const std::string s_ufssModeHelp;
+  static const std::string s_userPatModeHelp;
+  static const std::string s_errorSelectionRulesHelp;
+  static const std::string s_arithPropagationModeHelp;
+  static const std::string s_arithUnateLemmasHelp;
+
+
+}; /* class SmtOptionsHandler */
+
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SMT_OPTIONS_HANDLER_H */
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
deleted file mode 100644
index 376584636..000000000
--- a/src/smt/smt_options_template.cpp
+++ /dev/null
@@ -1,138 +0,0 @@
-/*********************                                                        */
-/*! \file smt_options_template.cpp
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Option handling for SmtEngine
- **
- ** Option handling for SmtEngine.
- **/
-
-#include "smt/smt_engine.h"
-#include "smt/modal_exception.h"
-#include "util/sexpr.h"
-#include "util/dump.h"
-#include "expr/command.h"
-#include "expr/node_manager.h"
-
-#include <string>
-#include <sstream>
-
-${include_all_option_headers}
-${option_handler_includes}
-
-#line 31 "${template}"
-
-using namespace std;
-
-namespace CVC4 {
-
-void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
-  throw(OptionException, ModalException) {
-
-  NodeManagerScope nms(d_nodeManager);
-  SmtEngine* const smt = this;
-
-  Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetOptionCommand(key, value);
-  }
-
-  if(key == "command-verbosity") {
-    if(!value.isAtom()) {
-      const vector<SExpr>& cs = value.getChildren();
-      if(cs.size() == 2 &&
-         (cs[0].isKeyword() || cs[0].isString()) &&
-         cs[1].isInteger()) {
-        string c = cs[0].getValue();
-        const Integer& v = cs[1].getIntegerValue();
-        if(v < 0 || v > 2) {
-          throw OptionException("command-verbosity must be 0, 1, or 2");
-        }
-        d_commandVerbosity[c] = v;
-        return;
-      }
-    }
-    throw OptionException("command-verbosity value must be a tuple (command-name, integer)");
-  }
-
-  if(!value.isAtom()) {
-    throw OptionException("bad value for :" + key);
-  }
-
-  string optionarg = value.getValue();
-
-  ${smt_setoption_handlers}
-
-#line 74 "${template}"
-
-  throw UnrecognizedOptionException(key);
-}
-
-CVC4::SExpr SmtEngine::getOption(const std::string& key) const
-  throw(OptionException) {
-
-  NodeManagerScope nms(d_nodeManager);
-
-  Trace("smt") << "SMT getOption(" << key << ")" << endl;
-
-  if(key.length() >= 18 &&
-     key.compare(0, 18, "command-verbosity:") == 0) {
-    map<string, Integer>::const_iterator i = d_commandVerbosity.find(key.c_str() + 18);
-    if(i != d_commandVerbosity.end()) {
-      return (*i).second;
-    }
-    i = d_commandVerbosity.find("*");
-    if(i != d_commandVerbosity.end()) {
-      return (*i).second;
-    }
-    return Integer(2);
-  }
-
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetOptionCommand(key);
-  }
-
-  if(key == "command-verbosity") {
-    vector<SExpr> result;
-    SExpr defaultVerbosity;
-    for(map<string, Integer>::const_iterator i = d_commandVerbosity.begin();
-        i != d_commandVerbosity.end();
-        ++i) {
-      vector<SExpr> v;
-      v.push_back((*i).first);
-      v.push_back((*i).second);
-      if((*i).first == "*") {
-        // put the default at the end of the SExpr
-        defaultVerbosity = v;
-      } else {
-        result.push_back(v);
-      }
-    }
-    // put the default at the end of the SExpr
-    if(!defaultVerbosity.isAtom()) {
-      result.push_back(defaultVerbosity);
-    } else {
-      // ensure the default is always listed
-      vector<SExpr> v;
-      v.push_back("*");
-      v.push_back(Integer(2));
-      result.push_back(v);
-    }
-    return result;
-  }
-
-  ${smt_getoption_handlers}
-
-#line 134 "${template}"
-
-  throw UnrecognizedOptionException(key);
-}
-
-}/* CVC4 namespace */