Options merge. This commit:

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

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

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

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

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

Benefits of the new options system include:

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

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

8 files changed, 641 insertions, 194 deletions

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 5cc0cedd1..9cc236a13 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -12,9 +12,16 @@ libsmt_la_SOURCES = \
 	smt_engine_scope.h \
 	modal_exception.h \
 	bad_option_exception.h \
-	no_such_function_exception.h
+	no_such_function_exception.h \
+	simplification_mode.h \
+	simplification_mode.cpp
+
+nodist_libsmt_la_SOURCES = \
+	smt_options.cpp
 
 EXTRA_DIST = \
+	options_handlers.h \
+	smt_options_template.cpp \
 	bad_option_exception.i \
 	no_such_function_exception.i \
 	modal_exception.i \
diff --git a/src/smt/options b/src/smt/options
new file mode 100644
index 000000000..5ee65e50a
--- /dev/null
+++ b/src/smt/options
@@ -0,0 +1,81 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+# FIXME: need to add support for SMT-LIBv2-required options:
+#
+#   expand-definitions
+#   regular-output-channel
+#   diagnostic-output-channel
+#   produce-unsat-cores
+#
+
+module SMT "smt/options.h" SMT layer
+
+common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
+ dump preprocessed assertions, etc., see --dump=help
+common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
+ all dumping goes to FILE (instead of stdout)
+
+expert-option lazyDefinitionExpansion --lazy-definition-expansion bool
+ expand define-funs/LAMBDAs lazily
+
+option simplificationMode --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 /--no-static-learning bool :default true
+ use static learning (on by default)
+/turn off static learning (e.g. diamond-breaking)
+
+common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
+ support the get-value and get-model commands
+common-option produceAssignments produce-assignments --produce-assignments bool
+ support the get-assignment command
+
+# This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
+# is a mode in which the assertion list must be kept.  So it belongs here.
+common-option interactive interactive-mode --interactive bool :read-write
+ force interactive mode
+
+option doITESimp --ite-simp bool :read-write
+ turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
+/turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)
+
+option unconstrainedSimp --unconstrained-simp bool :default false :read-write
+ turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
+/turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
+
+option repeatSimp --repeat-simp bool :read-write
+ make multiple passes with nonclausal simplifier
+/do not make multiple passes with nonclausal simplifier
+
+common-option incrementalSolving incremental -i --incremental bool
+ enable incremental solving
+
+common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long"
+ enable time limiting (give milliseconds)
+common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long"
+ enable time limiting per query (give milliseconds)
+common-option cumulativeResourceLimit --rlimit=N "unsigned long"
+ enable resource limiting
+common-option perCallResourceLimit --rlimit-per=N "unsigned long"
+ enable resource limiting per query
+
+option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
+ replay decisions from file
+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 threads --threads=N unsigned :default 2
+ Total number of threads
+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
+
+endmodule
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
new file mode 100644
index 000000000..f111f512b
--- /dev/null
+++ b/src/smt/options_handlers.h
@@ -0,0 +1,251 @@
+/*********************                                                        */
+/*! \file options_handlers.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief 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 "util/dump.h"
+
+namespace CVC4 {
+namespace smt {
+
+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 declarations.  Implied by all following modes.\n\
+\n\
+assertions\n\
++ Output the assertions after non-clausal simplification and static\n\
+  learning phases, but before presolve-time T-lemmas arrive.  If\n\
+  non-clausal simplification and static learning are off\n\
+  (--simplification=none --no-static-learning), the output\n\
+  will closely resemble the input (with term-level ITEs removed).\n\
+\n\
+learned\n\
++ Output the assertions after non-clausal simplification, static\n\
+  learning, and presolve-time T-lemmas.  This should include all eager\n\
+  T-lemmas (in the form provided by the theory, which my or may not be\n\
+  clausal).  Also includes level-0 BCP done by Minisat.\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\
+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, learned, 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\
+incremental\n\
++ run nonclausal simplification and clausal propagation at each ASSERT\n\
+  (and at CHECKSAT/QUERY/SUBTYPE)\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")) {
+    } else if(!strcmp(optargPtr, "learned")) {
+    } 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 {
+      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");
+    }
+  }
+  free(optargPtr);
+#else /* CVC4_DUMPING */
+  throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+inline void dumpToFile(std::string option, std::string optarg, SmtEngine* smt) {
+#ifdef CVC4_DUMPING
+  size_t dagSetting = expr::ExprDag::getDag(Dump.getStream());
+  if(optarg == "") {
+    throw OptionException(std::string("Bad file name for --dump-to"));
+  } else if(optarg == "-") {
+    Dump.setStream(DumpOutC::dump_cout);
+  } else {
+    std::ostream* dumpTo = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(!*dumpTo) {
+      throw OptionException(std::string("Cannot open dump-to file (maybe it exists): `") + optarg + "'");
+    }
+    Dump.setStream(*dumpTo);
+  }
+  expr::ExprDag::setDag(Dump.getStream(), dagSetting);
+#else /* CVC4_DUMPING */
+  throw OptionException("The dumping feature was disabled in this build of CVC4.");
+#endif /* CVC4_DUMPING */
+}
+
+inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "batch") {
+    return SIMPLIFICATION_MODE_BATCH;
+  } else if(optarg == "incremental") {
+    return SIMPLIFICATION_MODE_INCREMENTAL;
+  } else if(optarg == "none") {
+    return SIMPLIFICATION_MODE_NONE;
+  } else if(optarg == "help") {
+    puts(simplificationHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --simplification: `") +
+                          optarg + "'.  Try --simplification help.");
+  }
+}
+
+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 {
+    std::ostream* replayLog = new std::ofstream(optarg.c_str(), std::ofstream::out | std::ofstream::trunc);
+    if(!*replayLog) {
+      throw OptionException(std::string("Cannot open replay-log file: `") + optarg + "'");
+    }
+    return replayLog;
+  }
+#else /* CVC4_REPLAY */
+  throw OptionException("The replay feature was disabled in this build of CVC4.");
+#endif /* CVC4_REPLAY */
+}
+
+}/* 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
new file mode 100644
index 000000000..7bae74417
--- /dev/null
+++ b/src/smt/simplification_mode.cpp
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file simplification_mode.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ 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_INCREMENTAL:
+    out << "SIMPLIFICATION_MODE_INCREMENTAL";
+    break;
+  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
new file mode 100644
index 000000000..6e0faafc0
--- /dev/null
+++ b/src/smt/simplification_mode.h
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file simplification_mode.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#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 as they come in */
+  SIMPLIFICATION_MODE_INCREMENTAL,
+  /** 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 81a212edd..0acc53693 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -22,12 +22,16 @@
 #include <utility>
 #include <sstream>
 #include <stack>
+#include <cctype>
+#include <algorithm>
 #include <ext/hash_map>
 
 #include "context/cdlist.h"
 #include "context/cdhashset.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/expr.h"
 #include "expr/kind.h"
@@ -45,12 +49,15 @@
 #include "util/boolean_simplification.h"
 #include "util/configuration.h"
 #include "util/exception.h"
-#include "util/options.h"
+#include "smt/options.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/theory_traits.h"
 #include "theory/logic_info.h"
+#include "theory/options.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "util/ite_removal.h"
 #include "theory/model.h"
@@ -309,24 +316,24 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
   // first, some user-context-dependent TNodes might still exist
   // with rc == 0.
-  if(Options::current()->interactive ||
-     Options::current()->incrementalSolving) {
+  if(options::interactive() ||
+     options::incrementalSolving()) {
     // In the case of incremental solving, we appear to need these to
     // ensure the relevant Nodes remain live.
     d_assertionList = new(true) AssertionList(d_userContext);
   }
 
-  if(Options::current()->perCallResourceLimit != 0) {
-    setResourceLimit(Options::current()->perCallResourceLimit, false);
+  if(options::perCallResourceLimit() != 0) {
+    setResourceLimit(options::perCallResourceLimit(), false);
   }
-  if(Options::current()->cumulativeResourceLimit != 0) {
-    setResourceLimit(Options::current()->cumulativeResourceLimit, true);
+  if(options::cumulativeResourceLimit() != 0) {
+    setResourceLimit(options::cumulativeResourceLimit(), true);
   }
-  if(Options::current()->perCallMillisecondLimit != 0) {
-    setTimeLimit(Options::current()->perCallMillisecondLimit, false);
+  if(options::perCallMillisecondLimit() != 0) {
+    setTimeLimit(options::perCallMillisecondLimit(), false);
   }
-  if(Options::current()->cumulativeMillisecondLimit != 0) {
-    setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
+  if(options::cumulativeMillisecondLimit() != 0) {
+    setTimeLimit(options::cumulativeMillisecondLimit(), true);
   }
 }
 
@@ -380,7 +387,7 @@ SmtEngine::~SmtEngine() throw() {
   SmtScope smts(this);
 
   try {
-    while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) {
+    while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
       internalPop();
     }
 
@@ -456,28 +463,28 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
   d_logic.lock();
 
   // Set the options for the theoryOf
-  if(!Options::current()->theoryOfModeSetByUser) {
+  if(!options::theoryOfMode.wasSetByUser()) {
     if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {
       Theory::setTheoryOfMode(theory::THEORY_OF_TERM_BASED);
     } else {
       Theory::setTheoryOfMode(theory::THEORY_OF_TYPE_BASED);
     }
   } else {
-    Theory::setTheoryOfMode(Options::current()->theoryOfMode);
+    Theory::setTheoryOfMode(options::theoryOfMode());
   }
 
   // by default, symmetry breaker is on only for QF_UF
-  if(! Options::current()->ufSymmetryBreakerSetByUser) {
+  if(! options::ufSymmetryBreaker.wasSetByUser()) {
     bool qf_uf = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified();
     Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
-    NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf;
+    options::ufSymmetryBreaker.set(qf_uf);
   }
   // by default, nonclausal simplification is off for QF_SAT and for quantifiers
-  if(! Options::current()->simplificationModeSetByUser) {
+  if(! options::simplificationMode.wasSetByUser()) {
     bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
     bool quantifiers = d_logic.isQuantified();
     Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << std::endl;
-    NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat || quantifiers ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
+    options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH);
   }
 
   // If in arrays, set the UF handler to arrays
@@ -487,48 +494,48 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
     Theory::setUninterpretedSortOwner(THEORY_UF);
   }
   // Turn on ite simplification for QF_LIA and QF_AUFBV
-  if(! Options::current()->doITESimpSetByUser) {
+  if(! options::doITESimp.wasSetByUser()) {
     bool iteSimp = !d_logic.isQuantified() &&
       ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areRealsUsed()) ||
        (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)));
     Trace("smt") << "setting ite simplification to " << iteSimp << std::endl;
-    NodeManager::currentNM()->getOptions()->doITESimp = iteSimp;
+    options::doITESimp.set(iteSimp);
   }
   // Turn on multiple-pass non-clausal simplification for QF_AUFBV
-  if(! Options::current()->repeatSimpSetByUser) {
+  if(! options::repeatSimp.wasSetByUser()) {
     bool repeatSimp = !d_logic.isQuantified() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV));
     Trace("smt") << "setting repeat simplification to " << repeatSimp << std::endl;
-    NodeManager::currentNM()->getOptions()->repeatSimp = repeatSimp;
+    options::repeatSimp.set(repeatSimp);
   }
   // Turn on unconstrained simplification for QF_AUFBV
-  if(! Options::current()->unconstrainedSimpSetByUser || Options::current()->incrementalSolving) {
+  if(! options::unconstrainedSimp.wasSetByUser() || options::incrementalSolving()) {
     //    bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
-    //    bool uncSimp = false && !qf_sat && !Options::current()->incrementalSolving;
-    bool uncSimp = !Options::current()->incrementalSolving && !d_logic.isQuantified() &&
+    //    bool uncSimp = false && !qf_sat && !options::incrementalSolving();
+    bool uncSimp = !options::incrementalSolving() && !d_logic.isQuantified() &&
       (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_BV));
     Trace("smt") << "setting unconstrained simplification to " << uncSimp << std::endl;
-    NodeManager::currentNM()->getOptions()->unconstrainedSimp = uncSimp;
+    options::unconstrainedSimp.set(uncSimp);
   }
   // Turn on arith rewrite equalities only for pure arithmetic
-  if(! Options::current()->arithRewriteEqSetByUser) {
+  if(! options::arithRewriteEq.wasSetByUser()) {
     bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified();
     Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << std::endl;
-    NodeManager::currentNM()->getOptions()->arithRewriteEq = arithRewriteEq;
+    options::arithRewriteEq.set(arithRewriteEq);
   }
-  if(!  Options::current()->arithHeuristicPivotsSetByUser){
+  if(!  options::arithHeuristicPivots.wasSetByUser()) {
     int16_t heuristicPivots = 5;
-    if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
-      if(d_logic.isDifferenceLogic()){
+    if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()) {
+      if(d_logic.isDifferenceLogic()) {
         heuristicPivots = -1;
-      }else if(!d_logic.areIntegersUsed()){
+      } else if(!d_logic.areIntegersUsed()) {
         heuristicPivots = 0;
       }
     }
     Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << std::endl;
-    NodeManager::currentNM()->getOptions()->arithHeuristicPivots = heuristicPivots;
+    options::arithHeuristicPivots.set(heuristicPivots);
   }
-  if(! Options::current()->arithPivotThresholdSetByUser){
+  if(! options::arithPivotThreshold.wasSetByUser()){
     uint16_t pivotThreshold = 2;
     if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
       if(d_logic.isDifferenceLogic()){
@@ -536,24 +543,24 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
       }
     }
     Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << std::endl;
-    NodeManager::currentNM()->getOptions()->arithPivotThreshold = pivotThreshold;
+    options::arithPivotThreshold.set(pivotThreshold);
   }
-  if(! Options::current()->arithStandardCheckVarOrderPivotsSetByUser){
+  if(! options::arithStandardCheckVarOrderPivots.wasSetByUser()){
     int16_t varOrderPivots = -1;
     if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
       varOrderPivots = 200;
     }
     Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << std::endl;
-    NodeManager::currentNM()->getOptions()->arithStandardCheckVarOrderPivots = varOrderPivots;
+    options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
   }
   // Turn off early theory preprocessing if arithRewriteEq is on
-  if (NodeManager::currentNM()->getOptions()->arithRewriteEq) {
+  if (options::arithRewriteEq()) {
     d_earlyTheoryPP = false;
   }
   // Turn on justification heuristic of the decision engine for QF_BV and QF_AUFBV
   // and also use it in stop-only mode for QF_AUFLIA, QF_LRA and Quantifiers
-  if(!Options::current()->decisionModeSetByUser) {
-    Options::DecisionMode decMode =
+  if(!options::decisionMode.wasSetByUser()) {
+    decision::DecisionMode decMode =
       //QF_BV
       (not d_logic.isQuantified() &&
         d_logic.isPure(THEORY_BV)
@@ -576,8 +583,8 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
        ) ||
       // Quantifiers
       d_logic.isQuantified()
-      ? Options::DECISION_STRATEGY_JUSTIFICATION
-      : Options::DECISION_STRATEGY_INTERNAL;
+      ? decision::DECISION_STRATEGY_JUSTIFICATION
+      : decision::DECISION_STRATEGY_INTERNAL;
 
     bool stoponly =
       // QF_AUFLIA
@@ -595,12 +602,12 @@ void SmtEngine::setLogicInternal() throw(AssertionException) {
       ? true : false;
 
     Trace("smt") << "setting decision mode to " << decMode << std::endl;
-    NodeManager::currentNM()->getOptions()->decisionMode = decMode;
-    NodeManager::currentNM()->getOptions()->decisionOptions.stopOnly = stoponly;
+    options::decisionMode.set(decMode);
+    options::decisionStopOnly.set(stoponly);
   }
 }
 
-void SmtEngine::setInfo(const std::string& key, const SExpr& value)
+void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
   throw(BadOptionException, ModalException) {
 
   SmtScope smts(this);
@@ -636,15 +643,15 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
   }
 
   // Check for standard info keys (SMT-LIB v1, SMT-LIB v2, ...)
-  if(key == ":name" ||
-     key == ":source" ||
-     key == ":category" ||
-     key == ":difficulty" ||
-     key == ":smt-lib-version" ||
-     key == ":notes") {
+  if(key == "name" ||
+     key == "source" ||
+     key == "category" ||
+     key == "difficulty" ||
+     key == "smt-lib-version" ||
+     key == "notes") {
     // ignore these
     return;
-  } else if(key == ":status") {
+  } else if(key == "status") {
     string s;
     if(value.isAtom()) {
       s = value.getValue();
@@ -659,16 +666,24 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
   throw BadOptionException();
 }
 
-SExpr SmtEngine::getInfo(const std::string& key) const
+CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
   throw(BadOptionException, ModalException) {
 
   SmtScope smts(this);
 
   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
-  if(key == ":all-statistics") {
+  if(key == "all-statistics") {
     vector<SExpr> stats;
-    for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin();
-        i != StatisticsRegistry::end();
+    for(StatisticsRegistry::const_iterator i = d_exprManager->getStatisticsRegistry()->begin_();
+        i != d_exprManager->getStatisticsRegistry()->end_();
+        ++i) {
+      vector<SExpr> v;
+      v.push_back((*i)->getName());
+      v.push_back((*i)->getValue());
+      stats.push_back(v);
+    }
+    for(StatisticsRegistry::const_iterator i = d_statisticsRegistry->begin_();
+        i != d_statisticsRegistry->end_();
         ++i) {
       vector<SExpr> v;
       v.push_back((*i)->getName());
@@ -676,21 +691,32 @@ SExpr SmtEngine::getInfo(const std::string& key) const
       stats.push_back(v);
     }
     return stats;
-  } else if(key == ":error-behavior") {
+  } else if(key == "error-behavior") {
+    // immediate-exit | continued-execution
     return SExpr::Keyword("immediate-exit");
-  } else if(key == ":name") {
+  } else if(key == "name") {
     return Configuration::getName();
-  } else if(key == ":version") {
+  } else if(key == "version") {
     return Configuration::getVersionString();
-  } else if(key == ":authors") {
+  } else if(key == "authors") {
     return Configuration::about();
-  } else if(key == ":status") {
-    return d_status.asSatisfiabilityResult().toString();
-  } else if(key == ":reason-unknown") {
+  } else if(key == "status") {
+    // sat | unsat | unknown
+    switch(d_status.asSatisfiabilityResult().isSat()) {
+    case Result::SAT:
+      return SExpr::Keyword("sat");
+    case Result::UNSAT:
+      return SExpr::Keyword("unsat");
+    default:
+      return SExpr::Keyword("unknown");
+    }
+  } else if(key == "reason-unknown") {
     if(!d_status.isNull() && d_status.isUnknown()) {
       stringstream ss;
       ss << d_status.whyUnknown();
-      return SExpr::Keyword(ss.str());
+      string s = ss.str();
+      transform(s.begin(), s.end(), s.begin(), ::tolower);
+      return SExpr::Keyword(s);
     } else {
       throw ModalException("Can't get-info :reason-unknown when the "
                            "last result wasn't unknown!");
@@ -700,98 +726,6 @@ SExpr SmtEngine::getInfo(const std::string& key) const
   }
 }
 
-void SmtEngine::setOption(const std::string& key, const SExpr& value)
-  throw(BadOptionException, ModalException) {
-
-  SmtScope smts(this);
-
-  Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << SetOptionCommand(key, value);
-  }
-
-  if(key == ":print-success") {
-    if(value.isAtom() && value.getValue() == "false") {
-      *Options::current()->out << Command::printsuccess(false);
-    } else if(value.isAtom() && value.getValue() == "true") {
-      *Options::current()->out << Command::printsuccess(true);
-    } else {
-      throw BadOptionException();
-    }
-  } else if(key == ":expand-definitions") {
-    throw BadOptionException();
-  } else if(key == ":interactive-mode") {
-    throw BadOptionException();
-  } else if(key == ":regular-output-channel") {
-    throw BadOptionException();
-  } else if(key == ":diagnostic-output-channel") {
-    throw BadOptionException();
-  } else if(key == ":random-seed") {
-    throw BadOptionException();
-  } else if(key == ":verbosity") {
-    throw BadOptionException();
-  } else {
-    // The following options can only be set at the beginning; we throw
-    // a ModalException if someone tries.
-    if(d_logic.isLocked()) {
-      throw ModalException("logic already set; cannot set options");
-    }
-
-    if(key == ":produce-proofs") {
-      throw BadOptionException();
-    } else if(key == ":produce-unsat-cores") {
-      throw BadOptionException();
-    } else if(key == ":produce-models") {
-      //throw BadOptionException();
-      const_cast<Options*>( Options::s_current )->produceModels = true;
-    } else if(key == ":produce-assignments") {
-      throw BadOptionException();
-    } else {
-      throw BadOptionException();
-    }
-  }
-}
-
-SExpr SmtEngine::getOption(const std::string& key) const
-  throw(BadOptionException) {
-
-  SmtScope smts(this);
-
-  Trace("smt") << "SMT getOption(" << key << ")" << endl;
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetOptionCommand(key);
-  }
-  if(key == ":print-success") {
-    if(Command::printsuccess::getPrintSuccess(*Options::current()->out)) {
-      return SExpr("true");
-    } else {
-      return SExpr("false");
-    }
-  } else if(key == ":expand-definitions") {
-    throw BadOptionException();
-  } else if(key == ":interactive-mode") {
-    throw BadOptionException();
-  } else if(key == ":produce-proofs") {
-    throw BadOptionException();
-  } else if(key == ":produce-unsat-cores") {
-    throw BadOptionException();
-  } else if(key == ":produce-models") {
-    throw BadOptionException();
-  } else if(key == ":produce-assignments") {
-    throw BadOptionException();
-  } else if(key == ":regular-output-channel") {
-    return SExpr("stdout");
-  } else if(key == ":diagnostic-output-channel") {
-    return SExpr("stderr");
-  } else if(key == ":random-seed") {
-    throw BadOptionException();
-  } else if(key == ":verbosity") {
-    throw BadOptionException();
-  } else {
-    throw BadOptionException();
-  }
-}
-
 void SmtEngine::defineFunction(Expr func,
                                const std::vector<Expr>& formals,
                                Expr formula) {
@@ -805,7 +739,7 @@ void SmtEngine::defineFunction(Expr func,
   SmtScope smts(this);
 
   // type check body
-  Type formulaType = formula.getType(Options::current()->typeChecking);
+  Type formulaType = formula.getType(options::typeChecking());
 
   Type funcType = func.getType();
   // We distinguish here between definitions of constants and functions,
@@ -1151,8 +1085,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
   learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd-1];
 
-  if( Options::current()->incrementalSolving ||
-      Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL ) {
+  if( options::incrementalSolving() ||
+      options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
     // Keep substitutions
     SubstitutionMap::iterator pos = d_lastSubstitutionPos;
     if(pos == d_topLevelSubstitutions.end()) {
@@ -1306,7 +1240,7 @@ bool SmtEnginePrivate::simplifyAssertions()
 
     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
 
-    if(Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
+    if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       // Perform non-clausal simplification
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << "performing non-clausal simplification" << endl;
@@ -1338,7 +1272,7 @@ bool SmtEnginePrivate::simplifyAssertions()
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
     // ITE simplification
-    if(Options::current()->doITESimp) {
+    if(options::doITESimp()) {
       simpITE();
     }
 
@@ -1347,7 +1281,7 @@ bool SmtEnginePrivate::simplifyAssertions()
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
     // Unconstrained simplification
-    if(Options::current()->unconstrainedSimp) {
+    if(options::unconstrainedSimp()) {
       unconstrainedSimp();
     }
 
@@ -1355,7 +1289,7 @@ bool SmtEnginePrivate::simplifyAssertions()
     Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
     Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-    if(Options::current()->repeatSimp && Options::current()->simplificationMode != Options::SIMPLIFICATION_MODE_NONE) {
+    if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << " doing repeated simplification" << std::endl;
       d_assertionsToCheck.swap(d_assertionsToPreprocess);
@@ -1458,7 +1392,7 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
-  if(!Options::current()->lazyDefinitionExpansion) {
+  if(!options::lazyDefinitionExpansion()) {
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_definitionExpansionTime);
     hash_map<TNode, Node, TNodeHashFunction> cache;
@@ -1480,7 +1414,7 @@ void SmtEnginePrivate::processAssertions() {
 
   bool noConflict = simplifyAssertions();
 
-  if(Options::current()->doStaticLearning) {
+  if(options::doStaticLearning()) {
     // Perform static learning
     Trace("simplify") << "SmtEnginePrivate::simplify(): "
                       << "performing static learning" << endl;
@@ -1495,7 +1429,7 @@ void SmtEnginePrivate::processAssertions() {
     d_smt.d_numAssertionsPost += d_assertionsToCheck.size();
   }
 
-  if(Options::current()->repeatSimp) {
+  if(options::repeatSimp()) {
     d_assertionsToCheck.swap(d_assertionsToPreprocess);
     noConflict &= simplifyAssertions();
     if (noConflict) {
@@ -1583,13 +1517,13 @@ void SmtEnginePrivate::addFormula(TNode n)
   d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
 
   // If the mode of processing is incremental prepreocess and assert immediately
-  if (Options::current()->simplificationMode == Options::SIMPLIFICATION_MODE_INCREMENTAL) {
+  if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) {
     processAssertions();
   }
 }
 
 void SmtEngine::ensureBoolean(const BoolExpr& e) {
-  Type type = e.getType(Options::current()->typeChecking);
+  Type type = e.getType(options::typeChecking());
   Type boolType = d_exprManager->booleanType();
   if(type != boolType) {
     stringstream ss;
@@ -1610,7 +1544,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
   Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
 
-  if(d_queryMade && !Options::current()->incrementalSolving) {
+  if(d_queryMade && !options::incrementalSolving()) {
     throw ModalException("Cannot make multiple queries unless "
                          "incremental solving is enabled "
                          "(try --incremental)");
@@ -1673,7 +1607,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 
   Trace("smt") << "SMT query(" << e << ")" << endl;
 
-  if(d_queryMade && !Options::current()->incrementalSolving) {
+  if(d_queryMade && !options::incrementalSolving()) {
     throw ModalException("Cannot make multiple queries unless "
                          "incremental solving is enabled "
                          "(try --incremental)");
@@ -1738,7 +1672,7 @@ Expr SmtEngine::simplify(const Expr& e) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
-  if( Options::current()->typeChecking ) {
+  if( options::typeChecking() ) {
     e.getType(true);// ensure expr is type-checked at this point
   }
   Trace("smt") << "SMT simplify(" << e << ")" << endl;
@@ -1754,13 +1688,13 @@ Expr SmtEngine::getValue(const Expr& e)
   SmtScope smts(this);
 
   // ensure expr is type-checked at this point
-  Type type = e.getType(Options::current()->typeChecking);
+  Type type = e.getType(options::typeChecking());
 
   Trace("smt") << "SMT getValue(" << e << ")" << endl;
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetValueCommand(e);
   }
-  if(!Options::current()->produceModels) {
+  if(!options::produceModels()) {
     const char* msg =
       "Cannot get value when produce-models options is off.";
     throw ModalException(msg);
@@ -1799,7 +1733,7 @@ Expr SmtEngine::getValue(const Expr& e)
 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   SmtScope smts(this);
   finalOptionsAreSet();
-  Type type = e.getType(Options::current()->typeChecking);
+  Type type = e.getType(options::typeChecking());
   // must be Boolean
   CheckArgument( type.isBoolean(), e,
                  "expected Boolean-typed variable or function application "
@@ -1813,7 +1747,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
                    n.getMetaKind() == kind::metakind::VARIABLE ), e,
                  "expected variable or defined-function application "
                  "in addToAssignment(),\ngot %s", e.toString().c_str() );
-  if(!Options::current()->produceAssignments) {
+  if(!options::produceAssignments()) {
     return false;
   }
   if(d_assignments == NULL) {
@@ -1824,14 +1758,14 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   return true;
 }
 
-SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
+CVC4::SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getAssignment()" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssignmentCommand();
   }
-  if(!Options::current()->produceAssignments) {
+  if(!options::produceAssignments()) {
     const char* msg =
       "Cannot get the current assignment when "
       "produce-assignments option is off.";
@@ -1890,7 +1824,7 @@ void SmtEngine::addToModelType( Type& t ){
   Trace("smt") << "SMT addToModelType(" << t << ")" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
-  if( Options::current()->produceModels ) {
+  if( options::produceModels() ) {
     d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) );
   }
 }
@@ -1899,7 +1833,7 @@ void SmtEngine::addToModelFunction( Expr& e ){
   Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
-  if( Options::current()->produceModels ) {
+  if( options::produceModels() ) {
     d_theoryEngine->getModel()->addDefineFunction( e.getNode() );
   }
 }
@@ -1909,9 +1843,9 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
   Trace("smt") << "SMT getModel()" << endl;
   SmtScope smts(this);
 
-  if(!Options::current()->produceModels) {
+  if(!options::produceModels()) {
     const char* msg =
-      "Cannot get value when produce-models options is off.";
+      "Cannot get model when produce-models options is off.";
     throw ModalException(msg);
   }
   if(d_status.isNull() ||
@@ -1934,7 +1868,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
     Dump("benchmark") << GetProofCommand();
   }
 #ifdef CVC4_PROOF
-  if(!Options::current()->proof) {
+  if(!options::proof()) {
     const char* msg =
       "Cannot get a proof when produce-proofs option is off.";
     throw ModalException(msg);
@@ -1960,7 +1894,7 @@ vector<Expr> SmtEngine::getAssertions()
   }
   SmtScope smts(this);
   Trace("smt") << "SMT getAssertions()" << endl;
-  if(!Options::current()->interactive) {
+  if(!options::interactive()) {
     const char* msg =
       "Cannot query the current assertion list when not in interactive mode.";
     throw ModalException(msg);
@@ -1983,7 +1917,7 @@ void SmtEngine::push() {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PushCommand();
   }
-  if(!Options::current()->incrementalSolving) {
+  if(!options::incrementalSolving()) {
     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
   }
 
@@ -2006,7 +1940,7 @@ void SmtEngine::pop() {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PopCommand();
   }
-  if(!Options::current()->incrementalSolving) {
+  if(!options::incrementalSolving()) {
     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
   }
   if(d_userContext->getLevel() == 0) {
@@ -2039,7 +1973,7 @@ void SmtEngine::pop() {
 void SmtEngine::internalPush() {
   Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPush()" << endl;
-  if(Options::current()->incrementalSolving) {
+  if(options::incrementalSolving()) {
     d_private->processAssertions();
     d_userContext->push();
     d_context->push();
@@ -2050,7 +1984,7 @@ void SmtEngine::internalPush() {
 void SmtEngine::internalPop() {
   Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPop()" << endl;
-  if(Options::current()->incrementalSolving) {
+  if(options::incrementalSolving()) {
     d_propEngine->pop();
     d_context->pop();
     d_userContext->pop();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index efb2425a1..5f0511894 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -34,7 +34,7 @@
 #include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
 #include "util/hash.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/stats.h"
@@ -302,25 +302,25 @@ public:
   /**
    * Set information about the script executing.
    */
-  void setInfo(const std::string& key, const SExpr& value)
+  void setInfo(const std::string& key, const CVC4::SExpr& value)
     throw(BadOptionException, ModalException);
 
   /**
    * Query information about the SMT environment.
    */
-  SExpr getInfo(const std::string& key) const
+  CVC4::SExpr getInfo(const std::string& key) const
     throw(BadOptionException, ModalException);
 
   /**
    * Set an aspect of the current SMT execution environment.
    */
-  void setOption(const std::string& key, const SExpr& value)
+  void setOption(const std::string& key, const CVC4::SExpr& value)
     throw(BadOptionException, ModalException);
 
   /**
    * Get an aspect of the current SMT execution environment.
    */
-  SExpr getOption(const std::string& key) const
+  CVC4::SExpr getOption(const std::string& key) const
     throw(BadOptionException);
 
   /**
@@ -388,7 +388,7 @@ public:
    * INVALID query).  Only permitted if the SmtEngine is set to
    * operate interactively and produce-assignments is on.
    */
-  SExpr getAssignment() throw(ModalException, AssertionException);
+  CVC4::SExpr getAssignment() throw(ModalException, AssertionException);
 
   /**
    * Add to Model Type.  This is used for recording which types should be reported
@@ -552,6 +552,17 @@ public:
   }
 
   /**
+   * Used as a predicate for options preprocessor.
+   */
+  static void beforeSearch(std::string option, bool value, SmtEngine* smt) {
+    if(smt->d_queryMade || smt->d_problemExtended) {
+      std::stringstream ss;
+      ss << "cannot change option `" << option << "' after assertions have been made";
+      throw OptionException(ss.str());
+    }
+  }
+
+  /**
    * print model function (need this?)
    */
   void printModel( std::ostream& out, Model* m );
diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp
new file mode 100644
index 000000000..8c7fa1abf
--- /dev/null
+++ b/src/smt/smt_options_template.cpp
@@ -0,0 +1,78 @@
+/*********************                                                        */
+/*! \file smt_options_template.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Option handling for SmtEngine
+ **
+ ** Option handling for SmtEngine.
+ **/
+
+#include "smt/smt_engine.h"
+#include "smt/bad_option_exception.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 34 "${template}"
+
+using namespace std;
+
+namespace CVC4 {
+
+void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
+  throw(BadOptionException, 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);
+  }
+
+  stringstream ss;
+  ss << value;
+  string optarg = ss.str();
+
+  ${smt_setoption_handlers}
+
+#line 57 "${template}"
+
+  throw BadOptionException();
+}
+
+CVC4::SExpr SmtEngine::getOption(const std::string& key) const
+  throw(BadOptionException) {
+
+  NodeManagerScope nms(d_nodeManager);
+
+  Trace("smt") << "SMT getOption(" << key << ")" << endl;
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << GetOptionCommand(key);
+  }
+
+  ${smt_getoption_handlers}
+
+#line 74 "${template}"
+
+  throw BadOptionException();
+}
+
+}/* CVC4 namespace */