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.

13 files changed, 476 insertions, 32 deletions

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();