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.

65 files changed, 1189 insertions, 148 deletions

diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index 9d6939ac9..7a4cde04d 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -74,6 +74,7 @@ libtheory_la_LIBADD = \
 	@builddir@/rewriterules/librewriterules.la
 
 EXTRA_DIST = \
+	options_handlers.h \
 	rewriter_tables_template.h \
 	instantiator_tables_template.cpp \
 	theory_traits_template.h \
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 68b580c54..b71f07852 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -38,8 +38,15 @@ libarith_la_SOURCES = \
 	theory_arith.cpp \
 	dio_solver.h \
 	dio_solver.cpp \
+	arith_heuristic_pivot_rule.h \
+	arith_heuristic_pivot_rule.cpp \
+	arith_unate_lemma_mode.h \
+	arith_unate_lemma_mode.cpp \
+	arith_propagation_mode.h \
+	arith_propagation_mode.cpp \
 	theory_arith_instantiator.h \
 	theory_arith_instantiator.cpp
 
 EXTRA_DIST = \
-	kinds
+	kinds \
+	options_handlers.h
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.cpp b/src/theory/arith/arith_heuristic_pivot_rule.cpp
new file mode 100644
index 000000000..1a2958556
--- /dev/null
+++ b/src/theory/arith/arith_heuristic_pivot_rule.cpp
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file arith_heuristic_pivot_rule.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 "theory/arith/arith_heuristic_pivot_rule.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ArithHeuristicPivotRule rule) {
+  switch(rule) {
+  case MINIMUM:
+    out << "MINIMUM";
+    break;
+  case BREAK_TIES:
+    out << "BREAK_TIES";
+    break;
+  case MAXIMUM:
+    out << "MAXIMUM";
+    break;
+  default:
+    out << "ArithHeuristicPivotRule!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/arith_heuristic_pivot_rule.h b/src/theory/arith/arith_heuristic_pivot_rule.h
new file mode 100644
index 000000000..ef0f8cfe5
--- /dev/null
+++ b/src/theory/arith/arith_heuristic_pivot_rule.h
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file arith_heuristic_pivot_rule.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__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
+#define __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+typedef enum {
+  MINIMUM,
+  BREAK_TIES,
+  MAXIMUM
+} ArithHeuristicPivotRule;
+
+std::ostream& operator<<(std::ostream& out, ArithHeuristicPivotRule rule) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_HEURISTIC_PIVOT_RULE_H */
diff --git a/src/theory/arith/arith_propagation_mode.cpp b/src/theory/arith/arith_propagation_mode.cpp
new file mode 100644
index 000000000..08c56ad3b
--- /dev/null
+++ b/src/theory/arith/arith_propagation_mode.cpp
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file arith_propagation_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 "theory/arith/arith_propagation_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ArithPropagationMode mode) {
+  switch(mode) {
+  case NO_PROP:
+    out << "NO_PROP";
+    break;
+  case UNATE_PROP:
+    out << "UNATE_PROP";
+    break;
+  case BOUND_INFERENCE_PROP:
+    out << "BOUND_INFERENCE_PROP";
+    break;
+  case BOTH_PROP:
+    out << "BOTH_PROP";
+    break;
+  default:
+    out << "ArithPropagationMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/arith_propagation_mode.h b/src/theory/arith/arith_propagation_mode.h
new file mode 100644
index 000000000..507862415
--- /dev/null
+++ b/src/theory/arith/arith_propagation_mode.h
@@ -0,0 +1,40 @@
+/*********************                                                        */
+/*! \file arith_propagation_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__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
+#define __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+typedef enum {
+  NO_PROP,
+  UNATE_PROP,
+  BOUND_INFERENCE_PROP,
+  BOTH_PROP
+} ArithPropagationMode;
+
+std::ostream& operator<<(std::ostream& out, ArithPropagationMode rule) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_PROPAGATION_MODE_H */
diff --git a/src/theory/arith/arith_unate_lemma_mode.cpp b/src/theory/arith/arith_unate_lemma_mode.cpp
new file mode 100644
index 000000000..58f5d7850
--- /dev/null
+++ b/src/theory/arith/arith_unate_lemma_mode.cpp
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file arith_unate_lemma_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 "theory/arith/arith_unate_lemma_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode mode) {
+  switch(mode) {
+  case NO_PRESOLVE_LEMMAS:
+    out << "NO_PRESOLVE_LEMMAS";
+    break;
+  case INEQUALITY_PRESOLVE_LEMMAS:
+    out << "INEQUALITY_PRESOLVE_LEMMAS";
+    break;
+  case EQUALITY_PRESOLVE_LEMMAS:
+    out << "EQUALITY_PRESOLVE_LEMMAS";
+    break;
+  case ALL_PRESOLVE_LEMMAS:
+    out << "ALL_PRESOLVE_LEMMAS";
+    break;
+  default:
+    out << "ArithUnateLemmaMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/arith_unate_lemma_mode.h b/src/theory/arith/arith_unate_lemma_mode.h
new file mode 100644
index 000000000..71ee26ded
--- /dev/null
+++ b/src/theory/arith/arith_unate_lemma_mode.h
@@ -0,0 +1,40 @@
+/*********************                                                        */
+/*! \file arith_unate_lemma_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__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
+#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+
+typedef enum {
+  NO_PRESOLVE_LEMMAS,
+  INEQUALITY_PRESOLVE_LEMMAS,
+  EQUALITY_PRESOLVE_LEMMAS,
+  ALL_PRESOLVE_LEMMAS
+} ArithUnateLemmaMode;
+
+std::ostream& operator<<(std::ostream& out, ArithUnateLemmaMode rule) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */
diff --git a/src/theory/arith/options b/src/theory/arith/options
new file mode 100644
index 000000000..8b45a6da2
--- /dev/null
+++ b/src/theory/arith/options
@@ -0,0 +1,55 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module ARITH "theory/arith/options.h" Arithmetic theory
+
+option arithUnateLemmaMode --unate-lemmas=MODE ArithUnateLemmaMode :handler CVC4::theory::arith::stringToArithUnateLemmaMode :default ALL_PRESOLVE_LEMMAS :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_unate_lemma_mode.h"
+ determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)
+
+option arithPropagationMode --arith-prop=MODE ArithPropagationMode :handler CVC4::theory::arith::stringToArithPropagationMode :default BOTH_PROP :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_propagation_mode.h"
+ turns on arithmetic propagation (default is 'old', see --arith-prop=help)
+
+# The maximum number of difference pivots to do per invocation of simplex.
+# If this is negative, the number of pivots done is the number of variables.
+# If this is not set by the user, different logics are free to chose different
+# defaults.
+option arithHeuristicPivots --heuristic-pivots=N int16_t :default 0 :read-write
+ the number of times to apply the heuristic pivot rule; if N < 0, this defaults to the number of variables; if this is unset, this is tuned by the logic selection
+
+# The maximum number of variable order pivots to do per invocation of simplex.
+# If this is negative, the number of pivots done is unlimited.
+# If this is not set by the user, different logics are free to chose different
+# defaults.
+expert-option arithStandardCheckVarOrderPivots --standard-effort-variable-order-pivots=N int16_t :default -1 :read-write
+ limits the number of pivots in a single invocation of check() at a non-full effort level using Bland's pivot rule
+
+option arithHeuristicPivotRule --heuristic-pivot-rule=RULE ArithHeuristicPivotRule :handler CVC4::theory::arith::stringToArithHeuristicPivotRule :default MINIMUM :handler-include "theory/arith/options_handlers.h" :include "theory/arith/arith_heuristic_pivot_rule.h"
+ change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)
+
+# The number of pivots before simplex rechecks every basic variable for a conflict
+option arithSimplexCheckPeriod --simplex-check-period=N uint16_t :default 200
+ the number of pivots to do in simplex before rechecking for a conflict on all variables
+
+# This is the pivots per basic variable that can be done using heuristic choices
+# before variable order must be used.
+# If this is not set by the user, different logics are free to chose different
+# defaults.
+option arithPivotThreshold --pivot-threshold=N uint16_t :default 2 :read-write
+ sets the number of pivots using --pivot-rule per basic variable per simplex instance before using variable order
+
+option arithPropagateMaxLength --prop-row-length=N uint16_t :default 16
+ sets the maximum row length to be used in propagation
+
+option arithDioSolver /--disable-dio-solver bool :default true
+ use Linear Diophantine Equation solver (Griggio, JSAT 2012)
+/turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)
+
+# Whether to split (= x y) into (and (<= x y) (>= x y)) in
+# arithmetic preprocessing.
+option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-equalities bool :default false :read-write
+ turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
+/turns off the preprocessing rewrite turning equalities into a conjunction of inequalities
+
+endmodule
diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h
new file mode 100644
index 000000000..3eafe2ef0
--- /dev/null
+++ b/src/theory/arith/options_handlers.h
@@ -0,0 +1,124 @@
+/*********************                                                        */
+/*! \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 arithmetic options
+ **
+ ** Custom handlers and predicates for arithmetic options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H
+
+#include <string>
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+static const std::string arithPresolveLemmasHelp = "\
+Presolve lemmas are generated before SAT search begins using the relationship\n\
+of constant terms and polynomials.\n\
+Modes currently supported by the --arith-presolve-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\
+";
+
+static const std::string propagationModeHelp = "\
+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\
+";
+
+static const std::string heuristicPivotRulesHelp = "\
+This decides on the rule used by simplex during hueristic 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\
++min-break-ties\n\
+  The minimum violation with ties broken by variable order (total)\n\
++max\n\
+  The maximum violation the bound\n\
+";
+
+inline ArithUnateLemmaMode stringToArithUnateLemmaMode(std::string option, std::string optarg, SmtEngine* smt) 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(arithPresolveLemmasHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --unate-lemmas: `") +
+                          optarg + "'.  Try --unate-lemmas help.");
+  }
+}
+
+inline ArithPropagationMode stringToArithPropagationMode(std::string option, std::string optarg, SmtEngine* smt) 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(propagationModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --arith-prop: `") +
+                          optarg + "'.  Try --arith-prop help.");
+  }
+}
+
+inline ArithHeuristicPivotRule stringToArithHeuristicPivotRule(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "min") {
+    return MINIMUM;
+  } else if(optarg == "min-break-ties") {
+    return BREAK_TIES;
+  } else if(optarg == "max") {
+    return MAXIMUM;
+  } else if(optarg == "help") {
+    puts(heuristicPivotRulesHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --heuristic-pivot-rule: `") +
+                          optarg + "'.  Try --heuristic-pivot-rule help.");
+  }
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARITH__OPTIONS_HANDLERS_H */
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 63bb42e7a..e77067d61 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -19,6 +19,7 @@
 
 
 #include "theory/arith/simplex.h"
+#include "theory/arith/options.h"
 
 using namespace std;
 
@@ -41,14 +42,14 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
   d_pivotsInRound(),
   d_DELTA_ZERO(0,0)
 {
-  switch(Options::ArithHeuristicPivotRule rule = Options::current()->arithHeuristicPivotRule) {
-  case Options::MINIMUM:
+  switch(ArithHeuristicPivotRule rule = options::arithHeuristicPivotRule()) {
+  case MINIMUM:
     d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
     break;
-  case Options::BREAK_TIES:
+  case BREAK_TIES:
     d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
     break;
-  case Options::MAXIMUM:
+  case MAXIMUM:
     d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
     break;
   default:
@@ -262,13 +263,13 @@ Result::Sat SimplexDecisionProcedure::findModel(bool exactResult){
     }
   }
   static const bool verbose = false;
-  exactResult |= Options::current()->arithStandardCheckVarOrderPivots < 0;
-  const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : Options::current()->arithStandardCheckVarOrderPivots;
+  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
+  const uint32_t inexactResultsVarOrderPivots = exactResult ? 0 : options::arithStandardCheckVarOrderPivots();
 
-  uint32_t checkPeriod = Options::current()->arithSimplexCheckPeriod;
+  uint32_t checkPeriod = options::arithSimplexCheckPeriod();
   if(result == Result::SAT_UNKNOWN){
-    uint32_t numDifferencePivots = Options::current()->arithHeuristicPivots < 0 ?
-      d_numVariables + 1 : Options::current()->arithHeuristicPivots;
+    uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ?
+      d_numVariables + 1 : options::arithHeuristicPivots();
     // The signed to unsigned conversion is safe.
     uint32_t pivotsRemaining = numDifferencePivots;
     while(!d_queue.empty() &&
@@ -421,7 +422,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
 
     --remainingIterations;
 
-    bool useVarOrderPivot = d_pivotsInRound.count(x_i) >=  Options::current()->arithPivotThreshold;
+    bool useVarOrderPivot = d_pivotsInRound.count(x_i) >=  options::arithPivotThreshold();
     if(!useVarOrderPivot){
       d_pivotsInRound.add(x_i);
     }
@@ -429,7 +430,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
 
     Debug("playground") << "pivots in rounds: " <<  d_pivotsInRound.count(x_i)
                         << " use " << useVarOrderPivot
-                        << " threshold " << Options::current()->arithPivotThreshold
+                        << " threshold " << options::arithPivotThreshold()
                         << endl;
 
     PreferenceFunction pf = useVarOrderPivot ? minVarOrder : minBoundAndRowCount;
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 33c6537de..324f3b21b 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -60,7 +60,7 @@
 #include "context/cdlist.h"
 
 #include "util/dense_map.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/stats.h"
 #include "util/result.h"
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c68e9cf54..d55860c41 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -42,6 +42,8 @@
 #include "theory/arith/normal_form.h"
 #include "theory/model.h"
 
+#include "theory/arith/options.h"
+
 #include <stdint.h>
 
 using namespace std;
@@ -651,7 +653,7 @@ Node TheoryArith::ppRewrite(TNode atom) {
                                << a << endl;
   }
 
-  if (a.getKind() == kind::EQUAL  && Options::current()->arithRewriteEq) {
+  if (a.getKind() == kind::EQUAL  && options::arithRewriteEq()) {
     Node leq = NodeBuilder<2>(kind::LEQ) << a[0] << a[1];
     Node geq = NodeBuilder<2>(kind::GEQ) << a[0] << a[1];
     Node rewritten = Rewriter::rewrite(leq.andNode(geq));
@@ -1536,8 +1538,8 @@ void TheoryArith::check(Effort effortLevel){
 
   // This should be fine if sat or unknown
   if(!emmittedConflictOrSplit &&
-     (Options::current()->arithPropagationMode == Options::UNATE_PROP ||
-      Options::current()->arithPropagationMode == Options::BOTH_PROP)){
+     (options::arithPropagationMode() == UNATE_PROP ||
+      options::arithPropagationMode() == BOTH_PROP)){
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
     Assert(d_qflraStatus != Result::UNSAT);
 
@@ -1600,7 +1602,7 @@ void TheoryArith::check(Effort effortLevel){
 
   if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){
     Node possibleConflict = Node::null();
-    if(!emmittedConflictOrSplit && Options::current()->arithDioSolver){
+    if(!emmittedConflictOrSplit && options::arithDioSolver()){
       possibleConflict = callDioSolver();
       if(possibleConflict != Node::null()){
         revertOutOfConflict();
@@ -1610,7 +1612,7 @@ void TheoryArith::check(Effort effortLevel){
       }
     }
 
-    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->arithDioSolver){
+    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && options::arithDioSolver()){
       Node possibleLemma = dioCutting();
       if(!possibleLemma.isNull()){
         Debug("arith") << "dio cut   " << possibleLemma << endl;
@@ -1791,8 +1793,8 @@ Node TheoryArith::explain(TNode n) {
 void TheoryArith::propagate(Effort e) {
   // This uses model values for safety. Disable for now.
   if(d_qflraStatus == Result::SAT &&
-     (Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
-      Options::current()->arithPropagationMode == Options::BOTH_PROP)
+     (options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
+      options::arithPropagationMode() == BOTH_PROP)
      && hasAnyUpdates()){
     propagateCandidates();
   }else{
@@ -2039,21 +2041,21 @@ void TheoryArith::presolve(){
   }
 
   vector<Node> lemmas;
-  switch(Options::current()->arithUnateLemmaMode){
-  case Options::NO_PRESOLVE_LEMMAS:
+  switch(options::arithUnateLemmaMode()){
+  case NO_PRESOLVE_LEMMAS:
     break;
-  case Options::INEQUALITY_PRESOLVE_LEMMAS:
+  case INEQUALITY_PRESOLVE_LEMMAS:
     d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
     break;
-  case Options::EQUALITY_PRESOLVE_LEMMAS:
+  case EQUALITY_PRESOLVE_LEMMAS:
     d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
     break;
-  case Options::ALL_PRESOLVE_LEMMAS:
+  case ALL_PRESOLVE_LEMMAS:
     d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
     d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
     break;
   default:
-    Unhandled(Options::current()->arithUnateLemmaMode);
+    Unhandled(options::arithUnateLemmaMode());
   }
 
   vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
@@ -2063,7 +2065,7 @@ void TheoryArith::presolve(){
     d_out->lemma(lem);
   }
 
-  // if(Options::current()->arithUnateLemmaMode == Options::ALL_UNATE){
+  // if(options::arithUnateLemmaMode() == Options::ALL_UNATE){
   //   vector<Node> lemmas;
   //   d_constraintDatabase.outputAllUnateLemmas(lemmas);
   //   vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
@@ -2187,7 +2189,7 @@ void TheoryArith::propagateCandidates(){
   for(; i != end; ++i){
     ArithVar var = *i;
     if(d_tableau.isBasic(var) &&
-       d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= Options::current()->arithPropagateMaxLength){
+       d_tableau.getRowLength(d_tableau.basicToRowIndex(var)) <= options::arithPropagateMaxLength()){
       d_candidateBasics.softAdd(var);
     }else{
       Tableau::ColIterator basicIter = d_tableau.colIterator(var);
@@ -2197,7 +2199,7 @@ void TheoryArith::propagateCandidates(){
         ArithVar rowVar = d_tableau.rowIndexToBasic(ridx);
         Assert(entry.getColVar() == var);
         Assert(d_tableau.isBasic(rowVar));
-        if(d_tableau.getRowLength(ridx) <= Options::current()->arithPropagateMaxLength){
+        if(d_tableau.getRowLength(ridx) <= options::arithPropagateMaxLength()){
           d_candidateBasics.softAdd(rowVar);
         }
       }
diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp
index ab3a1548e..1682897ae 100644
--- a/src/theory/arith/theory_arith_instantiator.cpp
+++ b/src/theory/arith/theory_arith_instantiator.cpp
@@ -17,6 +17,7 @@
 #include "theory/arith/theory_arith_instantiator.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 
 using namespace std;
@@ -179,7 +180,7 @@ int InstStrategySimplex::process( Node f, Theory::Effort effort, int e ){
 
 InstantiatorTheoryArith::InstantiatorTheoryArith(context::Context* c, QuantifiersEngine* ie, Theory* th) :
 Instantiator( c, ie, th ){
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     addInstStrategy( new InstStrategySimplex( this, d_quantEngine ) );
   }
 }
@@ -191,7 +192,7 @@ void InstantiatorTheoryArith::preRegisterTerm( Node t ){
 void InstantiatorTheoryArith::assertNode( Node assertion ){
   Debug("quant-arith-assert") << "InstantiatorTheoryArith::check: " << assertion << std::endl;
   d_quantEngine->addTermToDatabase( assertion );
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
@@ -201,7 +202,7 @@ void InstantiatorTheoryArith::assertNode( Node assertion ){
 }
 
 void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort effort ){
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     Debug("quant-arith") << "Setting up simplex for instantiator... " << std::endl;
     d_instRows.clear();
     d_tableaux_term.clear();
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index e4c814660..8b8a5bd48 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -22,4 +22,5 @@ libarrays_la_SOURCES = \
 	theory_arrays_model.h \
 	theory_arrays_model.cpp
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds
diff --git a/src/theory/arrays/options b/src/theory/arrays/options
new file mode 100644
index 000000000..bf8afc589
--- /dev/null
+++ b/src/theory/arrays/options
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module ARRAYS "theory/arrays/options.h" Arrays theory
+
+endmodule
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index 67c42d124..f5a722737 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -17,6 +17,7 @@
 #include "theory/theory_engine.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays.h"
+#include "theory/quantifiers/options.h"
 #include "theory/rr_candidate_generator.h"
 
 using namespace std;
@@ -38,7 +39,7 @@ void InstantiatorTheoryArrays::preRegisterTerm( Node t ){
 void InstantiatorTheoryArrays::assertNode( Node assertion ){
   Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
   d_quantEngine->addTermToDatabase( assertion );
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am
index c591ef7fb..a68ee62cd 100644
--- a/src/theory/booleans/Makefile.am
+++ b/src/theory/booleans/Makefile.am
@@ -15,4 +15,5 @@ libbooleans_la_SOURCES = \
 	circuit_propagator.h \
 	circuit_propagator.cpp
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds
diff --git a/src/theory/booleans/options b/src/theory/booleans/options
new file mode 100644
index 000000000..ae14de58b
--- /dev/null
+++ b/src/theory/booleans/options
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module BOOLEANS "theory/booleans/options.h" Boolean theory
+
+endmodule
diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am
index 4b2d566b4..ad471bae7 100644
--- a/src/theory/builtin/Makefile.am
+++ b/src/theory/builtin/Makefile.am
@@ -13,4 +13,5 @@ libbuiltin_la_SOURCES = \
 	theory_builtin.h \
 	theory_builtin.cpp
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds
diff --git a/src/theory/builtin/options b/src/theory/builtin/options
new file mode 100644
index 000000000..699f361c9
--- /dev/null
+++ b/src/theory/builtin/options
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module BUILTIN "theory/builtin/options.h" Builtin theory
+
+endmodule
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 1f698de0f..669cbe9e0 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -32,4 +32,5 @@ libbv_la_SOURCES = \
 	theory_bv_rewriter.cpp \
 	cd_set_collection.h 
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 60a98e6e5..c86f14398 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -25,6 +25,7 @@
 #include "prop/sat_solver_factory.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv.h"
+#include "theory/bv/options.h"
 
 using namespace std;
 
@@ -98,7 +99,7 @@ void Bitblaster::bbAtom(TNode node) {
   // asserting that the atom is true iff the definition holds
   Node atom_definition = mkNode(kind::IFF, node, atom_bb);
 
-  if (!Options::current()->bitvectorEagerBitblast) {
+  if (!options::bitvectorEagerBitblast()) {
     d_cnfStream->convertAndAssert(atom_definition, true, false);
     d_bitblastedAtoms.insert(node);
   } else {
@@ -150,7 +151,7 @@ Node Bitblaster::bbOptimize(TNode node) {
 /// Public methods
 
 void Bitblaster::addAtom(TNode atom) {
-  if (!Options::current()->bitvectorEagerBitblast) {
+  if (!options::bitvectorEagerBitblast()) {
     d_cnfStream->ensureLiteral(atom);
     SatLiteral lit = d_cnfStream->getLiteral(atom);
     d_satSolver->addMarkerLiteral(lit);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 24d6b300b..b0d04f952 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -20,6 +20,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/bv/bitblaster.h"
+#include "theory/bv/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -57,7 +58,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
 
   //// Eager bit-blasting
-  if (Options::current()->bitvectorEagerBitblast) {
+  if (options::bitvectorEagerBitblast()) {
     for (unsigned i = 0; i < assertions.size(); ++i) {
       TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
       if (atom.getKind() != kind::BITVECTOR_BITOF) {
@@ -105,7 +106,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   }
 
   // solving
-  if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
+  if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) {
     Assert(!d_bv->inConflict());
     BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
     bool ok = d_bitblaster->solve();
diff --git a/src/theory/bv/options b/src/theory/bv/options
new file mode 100644
index 000000000..72db63c09
--- /dev/null
+++ b/src/theory/bv/options
@@ -0,0 +1,17 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module BV "theory/bv/options.h" Bitvector theory
+
+option bitvectorEagerBitblast --bitblast-eager bool
+ eagerly bitblast the bitvectors to the main SAT solver
+
+option bitvectorShareLemmas --bitblast-share-lemmas bool
+ share lemmas from the bitblasting solver with the main solver
+
+option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
+ check the bitblasting eagerly
+
+endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index da2dd77f6..b6dcc6662 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/valuation.h"
 #include "theory/bv/bitblaster.h"
+#include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
 
 using namespace CVC4;
@@ -69,7 +70,7 @@ TheoryBV::Statistics::~Statistics() {
 void TheoryBV::preRegisterTerm(TNode node) {
   BVDebug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
-  if (Options::current()->bitvectorEagerBitblast) {
+  if (options::bitvectorEagerBitblast()) {
     // don't use the equality engine in the eager bit-blasting
     return;
   }
@@ -261,7 +262,7 @@ Node TheoryBV::explain(TNode node) {
 void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t);
-  if (!Options::current()->bitvectorEagerBitblast && d_useEqualityEngine) {
+  if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) {
     d_equalitySolver.addSharedTerm(t);
   }
 }
@@ -269,7 +270,7 @@ void TheoryBV::addSharedTerm(TNode t) {
 
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
-  if (Options::current()->bitvectorEagerBitblast) {
+  if (options::bitvectorEagerBitblast()) {
     return EQUALITY_UNKNOWN;
   }
 
diff --git a/src/theory/candidate_generator.cpp b/src/theory/candidate_generator.cpp
index a0f303c21..2563ef0d7 100644
--- a/src/theory/candidate_generator.cpp
+++ b/src/theory/candidate_generator.cpp
@@ -29,7 +29,7 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::inst;
 
 bool CandidateGenerator::isLegalCandidate( Node n ){
-  return ( !n.getAttribute(NoMatchAttribute()) && ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute()) ) );
+  return ( !n.getAttribute(NoMatchAttribute()) && ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute()) ) );
 }
 
 void CandidateGeneratorQueue::addCandidate( Node n ) {
diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am
index 8b5fbe979..b3aa318d5 100644
--- a/src/theory/datatypes/Makefile.am
+++ b/src/theory/datatypes/Makefile.am
@@ -14,4 +14,5 @@ libdatatypes_la_SOURCES = \
 	theory_datatypes_instantiator.h \
 	theory_datatypes_instantiator.cpp
 	
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
new file mode 100644
index 000000000..8a76e8134
--- /dev/null
+++ b/src/theory/datatypes/options
@@ -0,0 +1,8 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module DATATYPES "theory/datatypes/options.h" Datatypes theory
+
+endmodule
diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp
index b4b85c9fb..8ecf37fe2 100644
--- a/src/theory/datatypes/theory_datatypes_instantiator.cpp
+++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp
@@ -17,6 +17,7 @@
 #include "theory/datatypes/theory_datatypes_instantiator.h"
 #include "theory/datatypes/theory_datatypes.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/rr_candidate_generator.h"
 
@@ -35,7 +36,7 @@ Instantiator( c, ie, th ){
 void InstantiatorTheoryDatatypes::assertNode( Node assertion ){
   Debug("quant-datatypes-assert") << "InstantiatorTheoryDatatypes::check: " << assertion << std::endl;
   d_quantEngine->addTermToDatabase( assertion );
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
@@ -51,7 +52,7 @@ void InstantiatorTheoryDatatypes::processResetInstantiationRound( Theory::Effort
 
 int InstantiatorTheoryDatatypes::process( Node f, Theory::Effort effort, int e ){
   Debug("quant-datatypes") << "Datatypes: Try to solve (" << e << ") for " << f << "... " << std::endl;
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( e<2 ){
       return InstStrategy::STATUS_UNFINISHED;
     }else if( e==2 ){
diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp
index bad7e34cb..f7c21c555 100644
--- a/src/theory/inst_match.cpp
+++ b/src/theory/inst_match.cpp
@@ -20,6 +20,7 @@
 #include "theory/candidate_generator.h"
 #include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -106,7 +107,7 @@ void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
 }
 
 void InstMatch::makeInternal( QuantifiersEngine* qe ){
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
       if( it->second.hasAttribute(InstConstantAttribute()) ){
         d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
@@ -121,7 +122,7 @@ void InstMatch::makeInternal( QuantifiersEngine* qe ){
 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
     d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
-    if( Options::current()->cbqi && it->second.hasAttribute(InstConstantAttribute()) ){
+    if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
       d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
     }
   }
@@ -591,7 +592,7 @@ int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, Quantif
 }
 
 int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
-  Assert( Options::current()->eagerInstQuant );
+  Assert( options::eagerInstQuant() );
   if( !d_match_pattern.isNull() ){
     InstMatch m;
     if( getMatch( t, m, qe ) ){
@@ -808,7 +809,7 @@ void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe,
 }
 
 int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
-  Assert( Options::current()->eagerInstQuant );
+  Assert( options::eagerInstQuant() );
   int addedLemmas = 0;
   for( int i=0; i<(int)d_children.size(); i++ ){
     if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){
@@ -866,7 +867,7 @@ void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngin
 }
 
 int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
-  Assert( Options::current()->eagerInstQuant );
+  Assert( options::eagerInstQuant() );
   InstMatch m;
   for( int i=0; i<(int)t.getNumChildren(); i++ ){
     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
index ae11f429c..fb42909e0 100644
--- a/src/theory/ite_simplifier.h
+++ b/src/theory/ite_simplifier.h
@@ -39,7 +39,6 @@
 #include "theory/shared_terms_database.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
-#include "util/options.h"
 #include "util/stats.h"
 #include "util/hash.h"
 #include "util/cache.h"
diff --git a/src/theory/options b/src/theory/options
new file mode 100644
index 000000000..40d26472f
--- /dev/null
+++ b/src/theory/options
@@ -0,0 +1,14 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module THEORY "theory/options.h" Theory layer
+
+expert-option theoryRegistration /--no-theory-registration bool :default true
+ disable theory reg (not safe for some theories)
+
+expert-option theoryOfMode --theoryof-mode=MODE CVC4::theory::TheoryOfMode :handler CVC4::theory::stringToTheoryOfMode :handler-include "theory/options_handlers.h" :default CVC4::theory::THEORY_OF_TYPE_BASED :include "theory/theoryof_mode.h"
+ mode for theoryof
+
+endmodule
diff --git a/src/theory/options_handlers.h b/src/theory/options_handlers.h
new file mode 100644
index 000000000..b5c8a1fc0
--- /dev/null
+++ b/src/theory/options_handlers.h
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \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, 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 Custom handlers and predicates for TheoryEngine options
+ **
+ ** Custom handlers and predicates for TheoryEngine options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+
+static const std::string 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\
+";
+
+inline TheoryOfMode stringToTheoryOfMode(std::string option, std::string optarg, SmtEngine* smt) {
+  if(optarg == "type") {
+    return THEORY_OF_TYPE_BASED;
+  } else if(optarg == "term") {
+    return THEORY_OF_TERM_BASED;
+  } else if(optarg == "help") {
+    puts(theoryOfModeHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --theoryof-mode: `") +
+                          optarg + "'.  Try --theoryof-mode help.");
+  }
+}
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__OPTIONS_HANDLERS_H */
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index 316e2fbff..5172001fc 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -17,6 +17,10 @@ libquantifiers_la_SOURCES = \
 	instantiation_engine.cpp \
 	model_engine.h \
 	model_engine.cpp \
+	inst_when_mode.cpp \
+	inst_when_mode.h \
+	literal_match_mode.cpp \
+	literal_match_mode.h \
 	relevant_domain.h \
 	relevant_domain.cpp \
 	rep_set_iterator.h \
@@ -28,4 +32,6 @@ libquantifiers_la_SOURCES = \
 	model_builder.h \
 	model_builder.cpp
 
-EXTRA_DIST = kinds
\ No newline at end of file
+EXTRA_DIST = \
+	kinds \
+	options_handlers.h
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 1c6b47867..5d7317cbc 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -54,10 +54,10 @@ void FirstOrderModel::initialize(){
     initializeModelForTerm( f[1] );
   }
   //for debugging
-  if( Options::current()->printModelEngine ){
+  if( Trace.isOn("model-engine") ){
     for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){
       if( it->first.isSort() ){
-        Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+        Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
       }
     }
   }
@@ -181,4 +181,4 @@ void FirstOrderModel::toStream(std::ostream& out){
     out << std::endl;
   }
 #endif
-}
\ No newline at end of file
+}
diff --git a/src/theory/quantifiers/inst_when_mode.cpp b/src/theory/quantifiers/inst_when_mode.cpp
new file mode 100644
index 000000000..b60148c21
--- /dev/null
+++ b/src/theory/quantifiers/inst_when_mode.cpp
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file inst_when_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 <iostream>
+#include "theory/quantifiers/inst_when_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) {
+  switch(mode) {
+  case theory::quantifiers::INST_WHEN_PRE_FULL:
+    out << "INST_WHEN_PRE_FULL";
+    break;
+  case theory::quantifiers::INST_WHEN_FULL:
+    out << "INST_WHEN_FULL";
+    break;
+  case theory::quantifiers::INST_WHEN_FULL_LAST_CALL:
+    out << "INST_WHEN_FULL_LAST_CALL";
+    break;
+  case theory::quantifiers::INST_WHEN_LAST_CALL:
+    out << "INST_WHEN_LAST_CALL";
+    break;
+  default:
+    out << "InstWhenMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
+
diff --git a/src/theory/quantifiers/inst_when_mode.h b/src/theory/quantifiers/inst_when_mode.h
new file mode 100644
index 000000000..2cfba4935
--- /dev/null
+++ b/src/theory/quantifiers/inst_when_mode.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file inst_when_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_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H
+#define __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+typedef enum {
+  /** Apply instantiation round before full effort (possibly at standard effort) */
+  INST_WHEN_PRE_FULL,
+  /** Apply instantiation round at full effort or above  */
+  INST_WHEN_FULL,
+  /** Apply instantiation round at full effort half the time, and last call always */
+  INST_WHEN_FULL_LAST_CALL,
+  /** Apply instantiation round at last call only */
+  INST_WHEN_LAST_CALL,
+} InstWhenMode;
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__INST_WHEN_MODE_H */
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 2b79cd8b9..fb3e6fb36 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -18,6 +18,7 @@
 
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/first_order_model.h"
 
@@ -65,7 +66,7 @@ void InstantiationEngine::addCbqiLemma( Node f ){
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   //if counterexample-based quantifier instantiation is active
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     //check if any cbqi lemma has not been added yet
     bool addedLemma = false;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
@@ -136,9 +137,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
     return false;
   }else{
     Debug("inst-engine-ctrl") << "---Done. " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
-    if( Options::current()->printInstEngine ){
-      Message() << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
-    }
+    Trace("inst-engine") << "Added lemmas = " << (int)d_quantEngine->d_lemmas_waiting.size() << std::endl;
     //flush lemmas to output channel
     d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
     return true;
@@ -153,11 +152,11 @@ void InstantiationEngine::check( Theory::Effort e ){
   }
   //determine if we should perform check, based on instWhenMode
   bool performCheck = false;
-  if( Options::current()->instWhenMode==Options::INST_WHEN_FULL ){
+  if( options::instWhenMode()==INST_WHEN_FULL ){
     performCheck = ( e >= Theory::EFFORT_FULL );
-  }else if( Options::current()->instWhenMode==Options::INST_WHEN_FULL_LAST_CALL ){
+  }else if( options::instWhenMode()==INST_WHEN_FULL_LAST_CALL ){
     performCheck = ( ( e==Theory::EFFORT_FULL  && ierCounter%2==0 ) || e==Theory::EFFORT_LAST_CALL );
-  }else if( Options::current()->instWhenMode==Options::INST_WHEN_LAST_CALL ){
+  }else if( options::instWhenMode()==INST_WHEN_LAST_CALL ){
     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
   }else{
     performCheck = true;
@@ -165,9 +164,9 @@ void InstantiationEngine::check( Theory::Effort e ){
   if( performCheck ){
     Debug("inst-engine") << "IE: Check " << e << " " << ierCounter << std::endl;
     double clSet = 0;
-    if( Options::current()->printInstEngine ){
+    if( Trace.isOn("inst-engine") ){
       clSet = double(clock())/double(CLOCKS_PER_SEC);
-      Message() << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
+      Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl;
     }
     bool quantActive = false;
     //for each quantifier currently asserted,
@@ -178,7 +177,7 @@ void InstantiationEngine::check( Theory::Effort e ){
                          << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl;
     for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
       Node n = d_quantEngine->getModel()->getAssertedQuantifier( i );
-      if( Options::current()->cbqi && hasAddedCbqiLemma( n ) ){
+      if( options::cbqi() && hasAddedCbqiLemma( n ) ){
         Node cel = d_ce_lit[ n ];
         bool active, value;
         bool ceValue = false;
@@ -232,21 +231,21 @@ void InstantiationEngine::check( Theory::Effort e ){
             Debug("inst-engine") << "No instantiation given, returning unknown..." << std::endl;
             d_quantEngine->getOutputChannel().setIncomplete();
           }else{
-            Assert( Options::current()->finiteModelFind );
+            Assert( options::finiteModelFind() );
             Debug("inst-engine") << "No instantiation given, defer to another engine..." << std::endl;
           }
         }
       }
     }else{
       if( e==Theory::EFFORT_LAST_CALL ){
-        if( Options::current()->cbqi ){
+        if( options::cbqi() ){
           debugSat( SAT_CBQI );
         }
       }
     }
-    if( Options::current()->printInstEngine ){
+    if( Trace.isOn("inst-engine") ){
       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-      Message() << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
+      Trace("inst-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
     }
   }
 }
@@ -302,9 +301,9 @@ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){
 }
 
 bool InstantiationEngine::doCbqi( Node f ){
-  if( Options::current()->cbqiSetByUser ){
-    return Options::current()->cbqi;
-  }else if( Options::current()->cbqi ){
+  if( options::cbqi.wasSetByUser() ){
+    return options::cbqi();
+  }else if( options::cbqi() ){
     //if quantifier has a non-arithmetic variable, then do not use cbqi
     //if quantifier has an APPLY_UF term, then do not use cbqi
     return !hasNonArithmeticVariable( f ) && !hasApplyUf( f[1] );
diff --git a/src/theory/quantifiers/literal_match_mode.cpp b/src/theory/quantifiers/literal_match_mode.cpp
new file mode 100644
index 000000000..87b4b94fe
--- /dev/null
+++ b/src/theory/quantifiers/literal_match_mode.cpp
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file literal_match_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 <iostream>
+#include "theory/quantifiers/literal_match_mode.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) {
+  switch(mode) {
+  case theory::quantifiers::LITERAL_MATCH_NONE:
+    out << "LITERAL_MATCH_NONE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_PREDICATE:
+    out << "LITERAL_MATCH_PREDICATE";
+    break;
+  case theory::quantifiers::LITERAL_MATCH_EQUALITY:
+    out << "LITERAL_MATCH_EQUALITY";
+    break;
+  default:
+    out << "LiteralMatchMode!UNKNOWN";
+  }
+
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/theory/quantifiers/literal_match_mode.h b/src/theory/quantifiers/literal_match_mode.h
new file mode 100644
index 000000000..189f0a235
--- /dev/null
+++ b/src/theory/quantifiers/literal_match_mode.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file literal_match_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_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H
+#define __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H
+
+#include <iostream>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+typedef enum {
+  /** Do not consider polarity of patterns */
+  LITERAL_MATCH_NONE,
+  /** Consider polarity of boolean predicates only */
+  LITERAL_MATCH_PREDICATE,
+  /** Consider polarity of boolean predicates, as well as equalities */
+  LITERAL_MATCH_EQUALITY,
+} LiteralMatchMode;
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+
+std::ostream& operator<<(std::ostream& out, theory::quantifiers::LiteralMatchMode mode) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__LITERAL_MATCH_MODE_H */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 9cd5020fb..5d49c914f 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -90,11 +90,11 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
           }
         }
       }
-      if( Options::current()->printModelEngine ){
+      if( Trace.isOn("model-engine") ){
         if( d_addedLemmas>0 ){
-          Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+          Trace("model-engine") << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
         }else{
-          Message() << "No InstGen lemmas..." << std::endl;
+          Trace("model-engine") << "No InstGen lemmas..." << std::endl;
         }
       }
       Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
@@ -388,11 +388,11 @@ void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){
 }
 
 bool ModelEngineBuilder::optUseModel() {
-  return Options::current()->fmfModelBasedInst;
+  return options::fmfModelBasedInst();
 }
 
 bool ModelEngineBuilder::optInstGen(){
-  return Options::current()->fmfInstGen;
+  return options::fmfInstGen();
 }
 
 bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index ddaaa5b6f..4d91c8c95 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -21,6 +21,7 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/uf/theory_uf_instantiator.h"
+#include "theory/quantifiers/options.h"
 #include "theory/arrays/theory_arrays_model.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/term_database.h"
@@ -64,9 +65,9 @@ void ModelEngine::check( Theory::Effort e ){
     if( addedLemmas==0 ){
       //quantifiers are initialized, we begin an instantiation round
       double clSet = 0;
-      if( Options::current()->printModelEngine ){
+      if( Trace.isOn("model-engine") ){
         clSet = double(clock())/double(CLOCKS_PER_SEC);
-        Message() << "---Model Engine Round---" << std::endl;
+        Trace("model-engine") << "---Model Engine Round---" << std::endl;
       }
       Debug("fmf-model-debug") << "---Begin Instantiation Round---" << std::endl;
       ++(d_statistics.d_inst_rounds);
@@ -108,11 +109,11 @@ void ModelEngine::check( Theory::Effort e ){
         }
         Debug("fmf-model-debug") << "---> Added lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
         Debug("fmf-model-debug") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
-        if( Options::current()->printModelEngine ){
-          Message() << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
-          Message() << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+        if( Trace.isOn("model-engine") ){
+          Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
+          Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
           double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-          Message() << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
+          Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
         }
 #ifdef ME_PRINT_WARNINGS
         if( addedLemmas>10000 ){
@@ -145,11 +146,11 @@ void ModelEngine::assertNode( Node f ){
 }
 
 bool ModelEngine::optOneInstPerQuantRound(){
-  return Options::current()->fmfOneInstPerRound;
+  return options::fmfOneInstPerRound();
 }
 
 bool ModelEngine::optUseRelevantDomain(){
-  return Options::current()->fmfRelevantDomain;
+  return options::fmfRelevantDomain();
 }
 
 bool ModelEngine::optOneQuantPerRound(){
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
new file mode 100644
index 000000000..91e831092
--- /dev/null
+++ b/src/theory/quantifiers/options
@@ -0,0 +1,89 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
+
+# Whether to mini-scope quantifiers.
+# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
+# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
+option miniscopeQuant /--disable-miniscope-quant bool :default true
+ disable miniscope quantifiers
+
+# Whether to mini-scope quantifiers based on formulas with no free variables.
+# For example, forall x. ( P( x ) V Q ) will be rewritten to
+# ( forall x. P( x ) ) V Q
+option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true
+ disable miniscope quantifiers for ground subformulas
+
+# Whether to prenex (nested universal) quantifiers
+option prenexQuant /--disable-prenex-quant bool :default true
+ disable prenexing of quantified formulas
+
+# Whether to variable-eliminate quantifiers.
+# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
+#   forall y. P( c, y )
+option varElimQuant --var-elim-quant bool :default false
+ enable variable elimination of quantified formulas
+
+# Whether to CNF quantifier bodies
+option cnfQuant --cnf-quant bool :default false
+ apply CNF conversion to quantified formulas
+
+# Whether to pre-skolemize quantifier bodies.
+# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
+#   forall x. P( x ) => f( S( x ) ) = x
+option preSkolemQuant --pre-skolem-quant bool :default false
+ apply skolemization eagerly to bodies of quantified formulas
+
+# Whether to use smart triggers
+option smartTriggers /--disable-smart-triggers bool :default true
+ disable smart triggers
+
+# Whether to consider terms in the bodies of quantifiers for matching
+option registerQuantBodyTerms --register-quant-body-terms bool :default false
+ consider ground terms within bodies of quantified formulas for matching
+
+option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :include "theory/quantifiers/inst_when_mode.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
+ when to apply instantiation
+
+option eagerInstQuant --eager-inst-quant bool :default false
+ apply quantifier instantiation eagerly
+
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/literal_match_mode.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
+ choose literal matching mode
+
+option cbqi --enable-cbqi/--disable-cbqi bool :default false
+ turns on counterexample-based quantifier instantiation [off by default]
+/turns off counterexample-based quantifier instantiation
+
+option userPatternsQuant /--ignore-user-patterns bool :default true
+ ignore user-provided patterns for quantifier instantiation
+
+option flipDecision --enable-flip-decision/ bool :default false
+ turns on flip decision heuristic
+
+option finiteModelFind --finite-model-find bool :default false
+ use finite model finding heuristic for quantifier instantiation
+
+option ufssRegions /--disable-uf-ss-regions bool :default true
+ disable region-based method for discovering cliques and splits in uf strong solver
+option ufssEagerSplits --uf-ss-eager-split bool :default false
+ add splits eagerly for uf strong solver
+option ufssColoringSat --uf-ss-coloring-sat bool :default false
+ use coloring-based SAT heuristic for uf strong solver
+
+option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
+ disable model-based quantifier instantiation for finite model finding
+
+option fmfInstGen /--disable-fmf-inst-gen bool :default true
+ disable Inst-Gen instantiation techniques for finite model finding
+option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
+ only add one instantiation per quantifier per round for fmf
+option fmfInstEngine --fmf-inst-engine bool :default false
+ use instantiation engine in conjunction with finite model finding
+option fmfRelevantDomain --fmf-relevant-domain bool :default false
+ use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
+
+endmodule
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
new file mode 100644
index 000000000..24734e8c8
--- /dev/null
+++ b/src/theory/quantifiers/options_handlers.h
@@ -0,0 +1,111 @@
+/*********************                                                        */
+/*! \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-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_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H
+
+#include <string>
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+static const std::string instWhenHelp = "\
+Modes currently supported by the --inst-when option:\n\
+\n\
+full\n\
++ Run instantiation round at full effort, before theory combination.\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\
+last-call\n\
++ Run instantiation at last call effort, after theory combination.\n\
+\n\
+";
+
+static const std::string 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\
+";
+
+inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg == "pre-full") {
+    return INST_WHEN_PRE_FULL;
+  } else if(optarg == "full") {
+    return INST_WHEN_FULL;
+  } else if(optarg == "full-last-call") {
+    return INST_WHEN_FULL_LAST_CALL;
+  } else if(optarg == "last-call") {
+    return INST_WHEN_LAST_CALL;
+  } else if(optarg == "help") {
+    puts(instWhenHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --inst-when: `") +
+                          optarg + "'.  Try --inst-when help.");
+  }
+}
+
+inline void checkInstWhenMode(std::string option, InstWhenMode mode, SmtEngine* smt) throw(OptionException) {
+  if(mode == INST_WHEN_PRE_FULL) {
+    throw OptionException(std::string("Mode pre-full for ") + option + " is not supported in this release.");
+  }
+}
+
+inline LiteralMatchMode stringToLiteralMatchMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
+  if(optarg ==  "none") {
+    return LITERAL_MATCH_NONE;
+  } else if(optarg ==  "predicate") {
+    return LITERAL_MATCH_PREDICATE;
+  } else if(optarg ==  "equality") {
+    return LITERAL_MATCH_EQUALITY;
+  } else if(optarg ==  "help") {
+    puts(literalMatchHelp.c_str());
+    exit(1);
+  } else {
+    throw OptionException(std::string("unknown option for --literal-matching: `") +
+                          optarg + "'.  Try --literal-matching help.");
+  }
+}
+
+inline void checkLiteralMatchMode(std::string option, LiteralMatchMode mode, SmtEngine* smt) throw(OptionException) {
+  if(mode == LITERAL_MATCH_EQUALITY) {
+    throw OptionException(std::string("Mode equality for ") + option + " is not supported in this release.");
+  }
+}
+
+}/* CVC4::theory::quantifiers namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__OPTIONS_HANDLERS_H */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index c397e9d05..800fa910c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -690,14 +691,14 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit
 }
 
 bool QuantifiersRewriter::doMiniscopingNoFreeVar(){
-  return Options::current()->miniscopeQuantFreeVar;
+  return options::miniscopeQuantFreeVar();
 }
 
 bool QuantifiersRewriter::doMiniscopingAnd(){
-  if( Options::current()->miniscopeQuant ){
+  if( options::miniscopeQuant() ){
     return true;
   }else{
-    if( Options::current()->cbqi ){
+    if( options::cbqi() ){
       return true;
     }else{
       return false;
@@ -709,13 +710,13 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption,
   if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
   }else if( computeOption==COMPUTE_PRE_SKOLEM ){
-    return Options::current()->preSkolemQuant && !duringRewrite;
+    return options::preSkolemQuant() && !duringRewrite;
   }else if( computeOption==COMPUTE_PRENEX ){
-    return Options::current()->prenexQuant;
+    return options::prenexQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-    return Options::current()->varElimQuant;
+    return options::varElimQuant();
   }else if( computeOption==COMPUTE_CNF ){
-    return Options::current()->cnfQuant && !duringRewrite;// || Options::current()->finiteModelFind;
+    return options::cnfQuant() && !duringRewrite;// || options::finiteModelFind();
   }else{
     return false;
   }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 945c82bf9..bb8fafb14 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -61,7 +61,7 @@ void TermDb::addTermEfficient( Node n, std::set< Node >& added){
 
 void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
   //don't add terms in quantifier bodies
-  if( withinQuant && !Options::current()->registerQuantBodyTerms ){
+  if( withinQuant && !options::registerQuantBodyTerms() ){
     return;
   }
   if( d_processed.find( n )==d_processed.end() ){
@@ -82,7 +82,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
         uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
         for( int i=0; i<(int)n.getNumChildren(); i++ ){
           addTerm( n[i], added, withinQuant );
-          if( Options::current()->efficientEMatching ){
+          if( options::efficientEMatching() ){
             if( d_parents[n[i]][op].empty() ){
               //must add parent to equivalence class info
               Node nir = d_ith->getRepresentative( n[i] );
@@ -97,7 +97,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
               Assert(!getParents(n[i],op,i).empty());
             }
           }
-          if( Options::current()->eagerInstQuant ){
+          if( options::eagerInstQuant() ){
             if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
               int addedLemmas = 0;
               for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
@@ -115,7 +115,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
       }
     }
   }else{
-    if( Options::current()->efficientEMatching && !n.hasAttribute(InstConstantAttribute())){
+    if( options::efficientEMatching() && !n.hasAttribute(InstConstantAttribute())){
       //Efficient e-matching must be notified
       //The term in triggers are not important here
       Debug("term-db") << "New in this branch term " << n << std::endl;
@@ -196,7 +196,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     Node mbt;
     if( d_type_map[ tn ].empty() ){
       std::stringstream ss;
-      ss << Expr::setlanguage(Options::current()->outputLanguage);
+      ss << Expr::setlanguage(options::outputLanguage());
       ss << "e_" << tn;
       mbt = NodeManager::currentNM()->mkVar( ss.str(), tn );
     }else{
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 27310e21b..3d41d28b7 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -27,6 +27,7 @@
 #include <map>
 #include <time.h>
 #include "theory/quantifiers/theory_quantifiers_instantiator.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 
 using namespace std;
diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
index 84b6c65c7..8486a3a84 100644
--- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
+++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp
@@ -16,6 +16,7 @@
 
 #include "theory/quantifiers/theory_quantifiers_instantiator.h"
 #include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/options.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -32,7 +33,7 @@ Instantiator( c, ie, th ){
 
 void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){
   Debug("quant-quant-assert") << "InstantiatorTheoryQuantifiers::check: " << assertion << std::endl;
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       Debug("quant-quant-assert") << "   -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl;
       setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 471bc9ac1..4d94d8d83 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -22,6 +22,7 @@
 #include "theory/arrays/theory_arrays.h"
 #include "theory/datatypes/theory_datatypes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/instantiation_engine.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -72,14 +73,14 @@ d_active( c ){
   d_model = new quantifiers::FirstOrderModel( this, c, "FirstOrderModel" );
 
   //add quantifiers modules
-  if( !Options::current()->finiteModelFind || Options::current()->fmfInstEngine ){
+  if( !options::finiteModelFind() || options::fmfInstEngine() ){
     //the instantiation must set incomplete flag unless finite model finding is turned on
-    d_inst_engine = new quantifiers::InstantiationEngine( this, !Options::current()->finiteModelFind );
+    d_inst_engine = new quantifiers::InstantiationEngine( this, !options::finiteModelFind() );
     d_modules.push_back(  d_inst_engine );
   }else{
     d_inst_engine = NULL;
   }
-  if( Options::current()->finiteModelFind ){
+  if( options::finiteModelFind() ){
     d_model_engine = new quantifiers::ModelEngine( this );
     d_modules.push_back( d_model_engine );
   }else{
@@ -130,7 +131,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
   }
   //build the model if not done so already
   //  this happens if no quantifiers are currently asserted and no model-building module is enabled
-  if( Options::current()->produceModels && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model_set ){
+  if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model_set ){
     d_te->getModelBuilder()->buildModel( d_model );
   }
 }
@@ -209,7 +210,7 @@ void QuantifiersEngine::registerQuantifier( Node f ){
       Node ceBody = d_term_db->getCounterexampleBody( quants[q] );
       generatePhaseReqs( quants[q], ceBody );
       //also register it with the strong solver
-      if( Options::current()->finiteModelFind ){
+      if( options::finiteModelFind() ){
         ((uf::TheoryUF*)d_te->getTheory( THEORY_UF ))->getStrongSolver()->registerQuantifier( quants[q] );
       }
     }
@@ -253,7 +254,7 @@ void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){
 void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){
     std::set< Node > added;
     getTermDatabase()->addTerm( n, added, withinQuant );
-    if( Options::current()->efficientEMatching ){
+    if( options::efficientEMatching() ){
       uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF );
       d_ith->newTerms(added);
     }
@@ -423,7 +424,7 @@ void QuantifiersEngine::flushLemmas( OutputChannel* out ){
 }
 
 void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
-  if( Options::current()->literalMatchMode!=Options::LITERAL_MATCH_NONE ){
+  if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE ){
     bool printed = false;
     // doing literal-based matching (consider polarity of literals)
     for( int i=0; i<(int)nodes.size(); i++ ){
diff --git a/src/theory/rewriterules/options b/src/theory/rewriterules/options
new file mode 100644
index 000000000..285e489be
--- /dev/null
+++ b/src/theory/rewriterules/options
@@ -0,0 +1,14 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module REWRITE_RULES "theory/rewriterules/options.h" Rewrite Rules
+
+option efficientEMatching --efficient-e-matching bool :default false
+ use efficient E-matching (only for rewrite rules)
+
+option rewriteRulesAsAxioms --rewrite-rules-as-axioms bool :default false
+ whether to convert rewrite rules to usual axioms (for debugging only)
+
+endmodule
diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp
index 57bc6d9cf..b4ae93653 100644
--- a/src/theory/rewriterules/theory_rewriterules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules.cpp
@@ -23,7 +23,7 @@
 
 #include "theory/rewriterules/theory_rewriterules_preprocess.h"
 #include "theory/rewriter.h"
-#include "util/options.h"
+#include "theory/rewriterules/options.h"
 
 
 using namespace std;
@@ -292,13 +292,13 @@ Trigger TheoryRewriteRules::createTrigger( TNode n, std::vector<Node> & pattern
   //  Debug("rewriterules") << "createTrigger:";
   getQuantifiersEngine()->registerPattern(pattern);
   return *Trigger::mkTrigger(getQuantifiersEngine(),n,pattern,
-                             Options::current()->efficientEMatching?
+                             options::efficientEMatching()?
                              Trigger::MATCH_GEN_EFFICIENT_E_MATCH :
                              Trigger::MATCH_GEN_DEFAULT,
                              true,
                              Trigger::TR_MAKE_NEW,
                              false);
-  //                             Options::current()->smartMultiTriggers);
+  //                             options::smartMultiTriggers());
 };
 
 bool TheoryRewriteRules::notifyIfKnown(const GList * const ltested,
diff --git a/src/theory/rewriterules/theory_rewriterules_rules.cpp b/src/theory/rewriterules/theory_rewriterules_rules.cpp
index 1ad8fdaa7..edea7a3c0 100644
--- a/src/theory/rewriterules/theory_rewriterules_rules.cpp
+++ b/src/theory/rewriterules/theory_rewriterules_rules.cpp
@@ -21,7 +21,7 @@
 #include "theory/rewriterules/theory_rewriterules_params.h"
 #include "theory/rewriterules/theory_rewriterules_preprocess.h"
 #include "theory/rewriterules/theory_rewriterules.h"
-#include "util/options.h"
+#include "theory/rewriterules/options.h"
 
 #include "theory/quantifiers/term_database.h"
 
@@ -110,7 +110,7 @@ inline void addPattern(TheoryRewriteRules & re,
   if (tri.getKind() == kind::NOT && tri[0].getKind() == kind::APPLY_UF)
     tri = tri[0];
   pattern.push_back(
-                    Options::current()->rewriteRulesAsAxioms?
+                    options::rewriteRulesAsAxioms()?
                     static_cast<Node>(tri):
                     re.getQuantifiersEngine()->getTermDatabase()->
                     convertNodeToPattern(tri,r,vars,inst_constants));
@@ -224,7 +224,7 @@ void TheoryRewriteRules::addRewriteRule(const Node r)
 
 
   //If we convert to usual axioms
-  if(Options::current()->rewriteRulesAsAxioms){
+  if(options::rewriteRulesAsAxioms()){
     NodeBuilder<> forallB(kind::FORALL);
     forallB << r[0];
     NodeBuilder<> guardsB(kind::AND);
diff --git a/src/theory/rr_inst_match.h b/src/theory/rr_inst_match.h
index d89b221bb..68b6e1bfd 100644
--- a/src/theory/rr_inst_match.h
+++ b/src/theory/rr_inst_match.h
@@ -35,6 +35,9 @@
 #include "expr/node_manager.h"
 #include "expr/node_builder.h"
 
+#include "theory/quantifiers/options.h"
+#include "theory/rewriterules/options.h"
+
 //#define USE_EFFICIENT_E_MATCHING
 
 namespace CVC4 {
@@ -65,8 +68,8 @@ public:
   /** legal candidate */
   static inline bool isLegalCandidate( TNode n ){
     return !n.getAttribute(NoMatchAttribute()) &&
-      ( !Options::current()->cbqi || !n.hasAttribute(InstConstantAttribute())) &&
-      ( !Options::current()->efficientEMatching || n.hasAttribute(AvailableInTermDb()) );
+      ( !options::cbqi() || !n.hasAttribute(InstConstantAttribute())) &&
+      ( !options::efficientEMatching() || n.hasAttribute(AvailableInTermDb()) );
 }
 
 };
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 24551637b..f3a9db394 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -32,7 +32,7 @@
 #include "context/context.h"
 #include "context/cdlist.h"
 #include "context/cdo.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/stats.h"
 #include "util/dump.h"
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1fb7305d4..6fbd4a417 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -24,7 +24,7 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "util/options.h"
+#include "options/options.h"
 #include "util/lemma_output_channel.h"
 
 #include "theory/theory.h"
@@ -38,6 +38,7 @@
 #include "theory/model.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/model_engine.h"
 #include "theory/quantifiers/first_order_model.h"
 
@@ -349,7 +350,7 @@ void TheoryEngine::check(Theory::Effort effort) {
       if( d_logicInfo.isQuantified() ){
         ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->performCheck(Theory::EFFORT_LAST_CALL);
         // if we have given up, then possibly flip decision
-        if(Options::current()->flipDecision) {
+        if(options::flipDecision()) {
           if(d_incomplete && !d_inConflict && !d_lemmasAdded) {
             if( ((theory::quantifiers::TheoryQuantifiers*) d_theoryTable[THEORY_QUANTIFIERS])->flipDecision() ) {
               d_incomplete = false;
@@ -357,7 +358,7 @@ void TheoryEngine::check(Theory::Effort effort) {
           }
         }
         //if returning incomplete or SAT, we have ensured that the model in the quantifiers engine has been built
-      }else if( Options::current()->produceModels ){
+      }else if( options::produceModels() ){
         //must build model at this point
         d_curr_model_builder->buildModel( d_curr_model );
       }
@@ -1114,8 +1115,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
   }
 
   // Share with other portfolio threads
-  if(Options::current()->lemmaOutputChannel != NULL) {
-    Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr());
+  if(options::lemmaOutputChannel() != NULL) {
+    options::lemmaOutputChannel()->notifyNewLemma(node.toExpr());
   }
 
   // Remove the ITEs
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 449f4adc3..de04c878c 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -36,7 +36,8 @@
 #include "theory/shared_terms_database.h"
 #include "theory/term_registration_visitor.h"
 #include "theory/valuation.h"
-#include "util/options.h"
+#include "options/options.h"
+#include "smt/options.h"
 #include "util/stats.h"
 #include "util/hash.h"
 #include "util/cache.h"
diff --git a/src/theory/trigger.cpp b/src/theory/trigger.cpp
index 92573d464..f895f6814 100644
--- a/src/theory/trigger.cpp
+++ b/src/theory/trigger.cpp
@@ -20,6 +20,7 @@
 #include "theory/uf/theory_uf_instantiator.h"
 #include "theory/candidate_generator.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/quantifiers/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -95,7 +96,7 @@ d_quantEngine( qe ), d_f( f ){
     ++(qe->d_statistics.d_multi_triggers);
   }
   //Notice() << "Trigger : " << (*this) << "  for " << f << std::endl;
-  if( Options::current()->eagerInstQuant ){
+  if( options::eagerInstQuant() ){
     Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF );
     uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator();
     for( int i=0; i<(int)d_nodes.size(); i++ ){
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 61330bbde..e027f8909 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -24,4 +24,6 @@ libuf_la_SOURCES = \
 	theory_uf_model.h \
 	theory_uf_model.cpp 
 
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+	kinds \
+	options_handlers.h
diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp
index 5696251ed..9d644ae8d 100644
--- a/src/theory/uf/inst_strategy.cpp
+++ b/src/theory/uf/inst_strategy.cpp
@@ -20,6 +20,7 @@
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 
 using namespace std;
@@ -144,9 +145,9 @@ void InstStrategyUserPatterns::addUserPattern( Node f, Node pat ){
     //extend to literal matching
     d_quantEngine->getPhaseReqTerms( f, nodes );
     //check match option
-    int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
     d_user_gen[f].push_back( Trigger::mkTrigger( d_quantEngine, f, nodes, matchOption, true, Trigger::TR_MAKE_NEW,
-                                                 Options::current()->smartTriggers ) );
+                                                 options::smartTriggers() ) );
   }
 }
 
@@ -298,11 +299,11 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       //}
     }
     //now, generate the trigger...
-    int matchOption = Options::current()->efficientEMatching ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
+    int matchOption = options::efficientEMatching() ? InstMatchGenerator::MATCH_GEN_EFFICIENT_E_MATCH : 0;
     Trigger* tr = NULL;
     if( d_is_single_trigger[ patTerms[0] ] ){
       tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL,
-                               Options::current()->smartTriggers );
+                               options::smartTriggers() );
       d_single_trigger_gen[ patTerms[0] ] = true;
     }else{
       //if we are re-generating triggers, shuffle based on some method
@@ -316,7 +317,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       }
       //will possibly want to get an old trigger
       tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD,
-                               Options::current()->smartTriggers );
+                               options::smartTriggers() );
     }
     if( tr ){
       if( tr->isMultiTrigger() ){
@@ -347,7 +348,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
             if( d_quantEngine->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
               d_single_trigger_gen[ patTerms[index] ] = true;
               Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL,
-                                                 Options::current()->smartTriggers );
+                                                 options::smartTriggers() );
               if( tr2 ){
                 //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
                 tr2->resetInstantiationRound();
diff --git a/src/theory/uf/options b/src/theory/uf/options
new file mode 100644
index 000000000..6f6900da0
--- /dev/null
+++ b/src/theory/uf/options
@@ -0,0 +1,12 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module UF "theory/uf/options.h" Uninterpreted functions theory
+
+option ufSymmetryBreaker uf-symmetry-breaker --enable-symmetry-breaker/--disable-symmetry-breaker bool :read-write :default true
+ use UF symmetry breaker (Deharbe et al., CADE 2011)
+/turns off UF symmetry breaker (Deharbe et al., CADE 2011)
+
+endmodule
diff --git a/src/theory/uf/options_handlers.h b/src/theory/uf/options_handlers.h
new file mode 100644
index 000000000..b08ae9d64
--- /dev/null
+++ b/src/theory/uf/options_handlers.h
@@ -0,0 +1,33 @@
+/*********************                                                        */
+/*! \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-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 Custom handlers and predicates for TheoryUF options
+ **
+ ** Custom handlers and predicates for TheoryUF options.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__UF__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__OPTIONS_HANDLERS_H */
+
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index d24878a62..5b8470567 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -18,6 +18,8 @@
  **/
 
 #include "theory/uf/theory_uf.h"
+#include "theory/uf/options.h"
+#include "theory/quantifiers/options.h"
 #include "theory/uf/theory_uf_instantiator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/model.h"
@@ -33,7 +35,7 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel&
   d_notify(*this),
   /* The strong theory solver can be notified by EqualityEngine::init(),
    * so make sure it's initialized first. */
-  d_thss(Options::current()->finiteModelFind ? new StrongSolverTheoryUf(c, u, out, this) : NULL),
+  d_thss(options::finiteModelFind() ? new StrongSolverTheoryUf(c, u, out, this) : NULL),
   d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"),
   d_conflict(c, false),
   d_literalsToPropagate(c),
@@ -179,7 +181,7 @@ void TheoryUF::presolve() {
   // TimerStat::CodeTimer codeTimer(d_presolveTimer);
 
   Debug("uf") << "uf: begin presolve()" << endl;
-  if(Options::current()->ufSymmetryBreaker) {
+  if(options::ufSymmetryBreaker()) {
     vector<Node> newClauses;
     d_symb.apply(newClauses);
     for(vector<Node>::const_iterator i = newClauses.begin();
@@ -299,7 +301,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
     }
   }
 
-  if(Options::current()->ufSymmetryBreaker) {
+  if(options::ufSymmetryBreaker()) {
     d_symb.assertFormula(n);
   }
 }/* TheoryUF::ppStaticLearn() */
diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp
index 48092b340..ea253cbdb 100644
--- a/src/theory/uf/theory_uf_instantiator.cpp
+++ b/src/theory/uf/theory_uf_instantiator.cpp
@@ -19,6 +19,8 @@
 #include "theory/uf/theory_uf.h"
 #include "theory/rr_candidate_generator.h"
 #include "theory/uf/equality_engine.h"
+#include "theory/quantifiers/options.h"
+#include "theory/rewriterules/options.h"
 #include "theory/quantifiers/term_database.h"
 
 using namespace std;
@@ -91,11 +93,11 @@ inline void outputEqClassInfo( const char* c, const EqClassInfo* eci){
 InstantiatorTheoryUf::InstantiatorTheoryUf(context::Context* c, CVC4::theory::QuantifiersEngine* qe, Theory* th) :
 Instantiator( c, qe, th )
 {
-  if( !Options::current()->finiteModelFind || Options::current()->fmfInstEngine ){
-    if( Options::current()->cbqi ){
+  if( !options::finiteModelFind() || options::fmfInstEngine() ){
+    if( options::cbqi() ){
       addInstStrategy( new InstStrategyCheckCESolved( this, qe ) );
     }
-    if( Options::current()->userPatternsQuant ){
+    if( options::userPatternsQuant() ){
       d_isup = new InstStrategyUserPatterns( this, qe );
       addInstStrategy( d_isup );
     }else{
@@ -106,7 +108,7 @@ Instantiator( c, qe, th )
     i_ag->setGenerateAdditional( true );
     addInstStrategy( i_ag );
     //addInstStrategy( new InstStrategyAddFailSplits( this, ie ) );
-    if( !Options::current()->finiteModelFind ){
+    if( !options::finiteModelFind() ){
       addInstStrategy( new InstStrategyFreeVariable( this, qe ) );
     }
     //d_isup->setPriorityOver( i_ag );
@@ -124,7 +126,7 @@ void InstantiatorTheoryUf::assertNode( Node assertion )
   Debug("quant-uf-assert") << "InstantiatorTheoryUf::check: " << assertion << std::endl;
   //preRegisterTerm( assertion );
   d_quantEngine->addTermToDatabase( assertion );
-  if( Options::current()->cbqi ){
+  if( options::cbqi() ){
     if( assertion.hasAttribute(InstConstantAttribute()) ){
       setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
     }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
@@ -337,7 +339,7 @@ void InstantiatorTheoryUf::newTerms(SetNode& s){
 
 /** merge */
 void InstantiatorTheoryUf::merge( TNode a, TNode b ){
-  if( Options::current()->efficientEMatching ){
+  if( options::efficientEMatching() ){
     //merge eqc_ops of b into a
     EqClassInfo* eci_a = getOrCreateEquivalenceClassInfo( a );
     EqClassInfo* eci_b = getOrCreateEquivalenceClassInfo( b );
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 895a7d056..70b07daa6 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -19,6 +19,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf_instantiator.h"
 #include "theory/theory_engine.h"
+#include "theory/quantifiers/options.h"
 #include "theory/quantifiers/term_database.h"
 
 //#define USE_SMART_SPLITS
@@ -194,7 +195,7 @@ struct sortExternalDegree {
 };
 
 bool StrongSolverTheoryUf::ConflictFind::Region::getMustCombine( int cardinality ){
-  if( Options::current()->ufssRegions && d_total_diseq_external>=long(cardinality) ){
+  if( options::ufssRegions() && d_total_diseq_external>=long(cardinality) ){
     //The number of external disequalities is greater than or equal to cardinality.
     //Thus, a clique of size cardinality+1 may exist between nodes in d_regions[i] and other regions
     //Check if this is actually the case:  must have n nodes with outgoing degree (cardinality+1-n) for some n>0
@@ -243,7 +244,7 @@ bool StrongSolverTheoryUf::ConflictFind::Region::check( Theory::Effort level, in
         }
       }
       return true;
-    }else if( Options::current()->ufssRegions || Options::current()->ufssEagerSplits || level==Theory::EFFORT_FULL ){
+    }else if( options::ufssRegions() || options::ufssEagerSplits() || level==Theory::EFFORT_FULL ){
       //build test clique, up to size cardinality+1
       if( d_testCliqueSize<=long(cardinality) ){
         std::vector< Node > newClique;
@@ -584,7 +585,7 @@ void StrongSolverTheoryUf::ConflictFind::explainClique( std::vector< Node >& cli
 /** new node */
 void StrongSolverTheoryUf::ConflictFind::newEqClass( Node n ){
   if( d_regions_map.find( n )==d_regions_map.end() ){
-    if( !Options::current()->ufssRegions ){
+    if( !options::ufssRegions() ){
       //if not using regions, always add new equivalence classes to region index = 0
       d_regions_index = 0;
     }
@@ -594,7 +595,7 @@ void StrongSolverTheoryUf::ConflictFind::newEqClass( Node n ){
     if( d_regions_index<d_regions.size() ){
       d_regions[ d_regions_index ]->debugPrint("uf-ss-debug",true);
       d_regions[ d_regions_index ]->d_valid = true;
-      Assert( !Options::current()->ufssRegions || d_regions[ d_regions_index ]->getNumReps()==0 );
+      Assert( !options::ufssRegions() || d_regions[ d_regions_index ]->getNumReps()==0 );
     }else{
       d_regions.push_back( new Region( this, d_th->getSatContext() ) );
     }
@@ -882,7 +883,7 @@ void StrongSolverTheoryUf::ConflictFind::check( Theory::Effort level, OutputChan
       }
       bool addedLemma = false;
       //do splitting on demand
-      if( level==Theory::EFFORT_FULL || Options::current()->ufssEagerSplits ){
+      if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){
         Debug("uf-ss-debug") << "Add splits?" << std::endl;
         //see if we have any recommended splits from large regions
         for( int i=0; i<(int)d_regions_index; i++ ){
@@ -902,7 +903,7 @@ void StrongSolverTheoryUf::ConflictFind::check( Theory::Effort level, OutputChan
       if( level==Theory::EFFORT_FULL ){
         if( !addedLemma ){
           Debug("uf-ss") << "No splits added." << std::endl;
-          if( Options::current()->ufssColoringSat ){
+          if( options::ufssColoringSat() ){
             //otherwise, try to disambiguate individual terms
             if( !disambiguateTerms( out ) ){
               //no disequalities can be propagated
@@ -1000,7 +1001,7 @@ void StrongSolverTheoryUf::ConflictFind::setCardinality( int c, OutputChannel* o
 }
 
 void StrongSolverTheoryUf::ConflictFind::getRepresentatives( std::vector< Node >& reps ){
-  if( !Options::current()->ufssColoringSat ){
+  if( !options::ufssColoringSat() ){
     bool foundRegion = false;
     for( int i=0; i<(int)d_regions_index; i++ ){
       //should not have multiple regions at this point
@@ -1045,7 +1046,7 @@ Node StrongSolverTheoryUf::ConflictFind::getCardinalityLemma(){
   if( d_cardinality_lemma.find( d_cardinality )==d_cardinality_lemma.end() ){
     if( d_cardinality_lemma_term.isNull() ){
       std::stringstream ss;
-      ss << Expr::setlanguage(Options::current()->outputLanguage);
+      ss << Expr::setlanguage(options::outputLanguage());
       ss << "t_" << d_type;
       d_cardinality_lemma_term = NodeManager::currentNM()->mkVar( ss.str(), d_type );
     }