Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.

57 files changed, 728 insertions, 470 deletions

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 8173f2cea..983fa2b30 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -78,7 +78,7 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
     }
   }
   d_errorSet.reduceToSignals();
-  d_errorSet.setSelectionRule(VAR_ORDER);
+  d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
 
   static int instance = 0;
   ++instance;
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 47a196353..bcb90f8ae 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -73,7 +73,7 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
 
   // We need to reduce this because of
   d_errorSet.reduceToSignals();
-  d_errorSet.setSelectionRule(VAR_ORDER);
+  d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
 
   if(processSignals()){
     d_conflictVariables.purge();
@@ -121,7 +121,7 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
 
   if(!d_errorSet.errorEmpty() && result != Result::UNSAT){
     if(exactResult){
-      d_errorSet.setSelectionRule(VAR_ORDER);
+      d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
       while(!d_errorSet.errorEmpty() && result != Result::UNSAT){
         Assert(checkPeriod > 0);
         if(searchForFeasibleSolution(checkPeriod)){
@@ -129,7 +129,7 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
         }
       }
     }else if( options::arithStandardCheckVarOrderPivots() > 0){
-      d_errorSet.setSelectionRule(VAR_ORDER);
+      d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
       if(searchForFeasibleSolution(options::arithStandardCheckVarOrderPivots())){
         result = Result::UNSAT;
       }
diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp
index 80c1e03ec..12e352e4d 100644
--- a/src/theory/arith/error_set.cpp
+++ b/src/theory/arith/error_set.cpp
@@ -152,37 +152,43 @@ ErrorSet::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates);
 }
 
-ErrorSet::ErrorSet(ArithVariables& vars, TableauSizes tabSizes, BoundCountingLookup lookups):
-  d_variables(vars),
-  d_errInfo(),
-  d_selectionRule(VAR_ORDER),
-  d_focus(ComparatorPivotRule(this,d_selectionRule)),
-  d_outOfFocus(),
-  d_signals(),
-  d_tableauSizes(tabSizes),
-  d_boundLookup(lookups)
+ErrorSet::ErrorSet(ArithVariables& vars,
+                   TableauSizes tabSizes,
+                   BoundCountingLookup lookups)
+    : d_variables(vars),
+      d_errInfo(),
+      d_selectionRule(options::ErrorSelectionRule::VAR_ORDER),
+      d_focus(ComparatorPivotRule(this, d_selectionRule)),
+      d_outOfFocus(),
+      d_signals(),
+      d_tableauSizes(tabSizes),
+      d_boundLookup(lookups)
 {}
 
-ErrorSelectionRule ErrorSet::getSelectionRule() const{
+options::ErrorSelectionRule ErrorSet::getSelectionRule() const
+{
   return d_selectionRule;
 }
 
-void ErrorSet::recomputeAmount(ErrorInformation& ei, ErrorSelectionRule rule){
+void ErrorSet::recomputeAmount(ErrorInformation& ei,
+                               options::ErrorSelectionRule rule)
+{
   switch(rule){
-  case MINIMUM_AMOUNT:
-  case MAXIMUM_AMOUNT:
-    ei.setAmount(computeDiff(ei.getVariable()));
-    break;
-  case SUM_METRIC:
-    ei.setMetric(sumMetric(ei.getVariable()));
-    break;
-  case VAR_ORDER:
-    //do nothing
-    break;
+    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
+    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
+      ei.setAmount(computeDiff(ei.getVariable()));
+      break;
+    case options::ErrorSelectionRule::SUM_METRIC:
+      ei.setMetric(sumMetric(ei.getVariable()));
+      break;
+    case options::ErrorSelectionRule::VAR_ORDER:
+      // do nothing
+      break;
   }
 }
 
-void ErrorSet::setSelectionRule(ErrorSelectionRule rule){
+void ErrorSet::setSelectionRule(options::ErrorSelectionRule rule)
+{
   if(rule != getSelectionRule()){
     FocusSet into(ComparatorPivotRule(this, rule));
     FocusSet::const_iterator iter = d_focus.begin();
@@ -202,16 +208,17 @@ void ErrorSet::setSelectionRule(ErrorSelectionRule rule){
   Assert(getSelectionRule() == rule);
 }
 
-ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es, ErrorSelectionRule r):
-  d_errorSet(es), d_rule (r)
+ComparatorPivotRule::ComparatorPivotRule(const ErrorSet* es,
+                                         options::ErrorSelectionRule r)
+    : d_errorSet(es), d_rule(r)
 {}
 
 bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
   switch(d_rule){
-  case VAR_ORDER:
-    // This needs to be the reverse of the minVariableOrder
-    return v > u;
-  case SUM_METRIC:
+    case options::ErrorSelectionRule::VAR_ORDER:
+      // This needs to be the reverse of the minVariableOrder
+      return v > u;
+    case options::ErrorSelectionRule::SUM_METRIC:
     {
       uint32_t v_metric = d_errorSet->getMetric(v);
       uint32_t u_metric = d_errorSet->getMetric(u);
@@ -221,7 +228,7 @@ bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
         return v_metric > u_metric;
       }
     }
-  case MINIMUM_AMOUNT:
+    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
     {
       const DeltaRational& vamt = d_errorSet->getAmount(v);
       const DeltaRational& uamt = d_errorSet->getAmount(u);
@@ -232,7 +239,7 @@ bool ComparatorPivotRule::operator()(ArithVar v, ArithVar u) const {
         return cmp > 0;
       }
     }
-  case MAXIMUM_AMOUNT:
+    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
     {
       const DeltaRational& vamt = d_errorSet->getAmount(v);
       const DeltaRational& uamt = d_errorSet->getAmount(u);
@@ -251,18 +258,18 @@ void ErrorSet::update(ErrorInformation& ei){
   if(ei.inFocus()){
 
     switch(getSelectionRule()){
-    case MINIMUM_AMOUNT:
-    case MAXIMUM_AMOUNT:
-      ei.setAmount(computeDiff(ei.getVariable()));
-      d_focus.update(ei.getHandle(), ei.getVariable());
-      break;
-    case  SUM_METRIC:
-      ei.setMetric(sumMetric(ei.getVariable()));
-      d_focus.update(ei.getHandle(), ei.getVariable());
-      break;
-    case  VAR_ORDER:
-      //do nothing
-      break;
+      case options::ErrorSelectionRule::MINIMUM_AMOUNT:
+      case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
+        ei.setAmount(computeDiff(ei.getVariable()));
+        d_focus.update(ei.getHandle(), ei.getVariable());
+        break;
+      case options::ErrorSelectionRule::SUM_METRIC:
+        ei.setMetric(sumMetric(ei.getVariable()));
+        d_focus.update(ei.getHandle(), ei.getVariable());
+        break;
+      case options::ErrorSelectionRule::VAR_ORDER:
+        // do nothing
+        break;
     }
   }
 }
@@ -300,16 +307,16 @@ void ErrorSet::transitionVariableIntoError(ArithVar v) {
   ErrorInformation& ei = d_errInfo.get(v);
 
   switch(getSelectionRule()){
-  case MINIMUM_AMOUNT:
-  case MAXIMUM_AMOUNT:
-    ei.setAmount(computeDiff(v));
-    break;
-  case SUM_METRIC:
-    ei.setMetric(sumMetric(ei.getVariable()));
-    break;
-  case VAR_ORDER:
-    //do nothing
-    break;
+    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
+    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
+      ei.setAmount(computeDiff(v));
+      break;
+    case options::ErrorSelectionRule::SUM_METRIC:
+      ei.setMetric(sumMetric(ei.getVariable()));
+      break;
+    case options::ErrorSelectionRule::VAR_ORDER:
+      // do nothing
+      break;
   }
   ei.setInFocus(true);
   FocusSetHandle handle = d_focus.push(v);
@@ -330,16 +337,16 @@ void ErrorSet::addBackIntoFocus(ArithVar v) {
   ErrorInformation& ei = d_errInfo.get(v);
   Assert(!ei.inFocus());
   switch(getSelectionRule()){
-  case MINIMUM_AMOUNT:
-  case MAXIMUM_AMOUNT:
-    ei.setAmount(computeDiff(v));
-    break;
-  case SUM_METRIC:
-    ei.setMetric(sumMetric(v));
-    break;
-  case VAR_ORDER:
-    //do nothing
-    break;
+    case options::ErrorSelectionRule::MINIMUM_AMOUNT:
+    case options::ErrorSelectionRule::MAXIMUM_AMOUNT:
+      ei.setAmount(computeDiff(v));
+      break;
+    case options::ErrorSelectionRule::SUM_METRIC:
+      ei.setMetric(sumMetric(v));
+      break;
+    case options::ErrorSelectionRule::VAR_ORDER:
+      // do nothing
+      break;
   }
 
   ei.setInFocus(true);
@@ -428,25 +435,6 @@ DeltaRational ErrorSet::computeDiff(ArithVar v) const{
   return diff;
 }
 
-ostream& operator<<(ostream& out, ErrorSelectionRule rule) {
-  switch(rule) {
-  case VAR_ORDER:
-    out << "VAR_ORDER";
-    break;
-  case MINIMUM_AMOUNT:
-    out << "MINIMUM_AMOUNT";
-    break;
-  case MAXIMUM_AMOUNT:
-    out << "MAXIMUM_AMOUNT";
-    break;
-  case SUM_METRIC:
-    out << "SUM_METRIC";
-    break;
-  }
-
-  return out;
-}
-
 void ErrorSet::debugPrint(std::ostream& out) const {
   static int instance = 0;
   ++instance;
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 9e3e7c630..5599cd268 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -22,7 +22,7 @@
 
 #include <vector>
 
-#include "options/arith_heuristic_pivot_rule.h"
+#include "options/arith_options.h"
 #include "theory/arith/arithvar.h"
 #include "theory/arith/bound_counts.h"
 #include "theory/arith/callbacks.h"
@@ -69,13 +69,14 @@ class ComparatorPivotRule {
 private:
   const ErrorSet* d_errorSet;
 
-  ErrorSelectionRule d_rule;
-public:
+  options::ErrorSelectionRule d_rule;
+
+ public:
   ComparatorPivotRule();
-  ComparatorPivotRule(const ErrorSet* es, ErrorSelectionRule r);
+  ComparatorPivotRule(const ErrorSet* es, options::ErrorSelectionRule r);
 
   bool operator()(ArithVar v, ArithVar u) const;
-  ErrorSelectionRule getRule() const { return d_rule; }
+  options::ErrorSelectionRule getRule() const { return d_rule; }
 };
 
 // typedef boost::heap::d_ary_heap<
@@ -225,7 +226,7 @@ private:
    */
   ErrorInfoMap d_errInfo;
 
-  ErrorSelectionRule d_selectionRule;
+  options::ErrorSelectionRule d_selectionRule;
   /**
    * The ordered heap for the variables that are in ErrorSet.
    */
@@ -259,12 +260,12 @@ private:
 public:
   DeltaRational computeDiff(ArithVar x) const;
 private:
-  void recomputeAmount(ErrorInformation& ei, ErrorSelectionRule r);
+ void recomputeAmount(ErrorInformation& ei, options::ErrorSelectionRule r);
 
-  void update(ErrorInformation& ei);
-  void transitionVariableOutOfError(ArithVar v);
-  void transitionVariableIntoError(ArithVar v);
-  void addBackIntoFocus(ArithVar v);
+ void update(ErrorInformation& ei);
+ void transitionVariableOutOfError(ArithVar v);
+ void transitionVariableIntoError(ArithVar v);
+ void addBackIntoFocus(ArithVar v);
 
 public:
 
@@ -291,8 +292,8 @@ public:
   void pushErrorInto(ArithVarVec& vec) const;
   void pushFocusInto(ArithVarVec& vec) const;
 
-  ErrorSelectionRule getSelectionRule() const;
-  void setSelectionRule(ErrorSelectionRule rule);
+  options::ErrorSelectionRule getSelectionRule() const;
+  void setSelectionRule(options::ErrorSelectionRule rule);
 
   inline ArithVar topFocusVariable() const{
     Assert(!focusEmpty());
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 29177d3f4..125a24f5e 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -106,8 +106,7 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   d_errorSet.reduceToSignals();
 
   // We must start tracking NOW
-  d_errorSet.setSelectionRule(SUM_METRIC);
-
+  d_errorSet.setSelectionRule(options::ErrorSelectionRule::SUM_METRIC);
 
   if(initialProcessSignals()){
     d_conflictVariables.purge();
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index ff2ec412b..e8b1b3b93 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -583,7 +583,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
       Trace("nl-ext-et-debug")
           << "Check entailment of " << ch_lemma << "..." << std::endl;
       std::pair<bool, Node> et = d_containing.getValuation().entailmentCheck(
-          THEORY_OF_TYPE_BASED, ch_lemma);
+          options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma);
       Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " "
                                << et.second << std::endl;
       if (et.first)
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 56a9bc95f..5bd6034d2 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -79,7 +79,7 @@ protected:
   DenseSet d_conflictVariables;
 
   /** The rule to use for heuristic selection mode. */
-  ErrorSelectionRule d_heuristicRule;
+  options::ErrorSelectionRule d_heuristicRule;
 
   /** Linear equality module. */
   LinearEqualityModule& d_linEq;
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index e50d9d060..1876f4b88 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -117,7 +117,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
   d_errorSet.reduceToSignals();
 
   // We must start tracking NOW
-  d_errorSet.setSelectionRule(SUM_METRIC);
+  d_errorSet.setSelectionRule(options::ErrorSelectionRule::SUM_METRIC);
 
   if(initialProcessSignals()){
     d_conflictVariables.purge();
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 58636a10b..b8bdd04e1 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3736,9 +3736,12 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
                       << "post approx cuts" << endl;
 
   // This should be fine if sat or unknown
-  if(!emmittedConflictOrSplit &&
-     (options::arithPropagationMode() == UNATE_PROP ||
-      options::arithPropagationMode() == BOTH_PROP)){
+  if (!emmittedConflictOrSplit
+      && (options::arithPropagationMode()
+              == options::ArithPropagationMode::UNATE_PROP
+          || options::arithPropagationMode()
+                 == options::ArithPropagationMode::BOTH_PROP))
+  {
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
     Assert(d_qflraStatus != Result::UNSAT);
 
@@ -3789,7 +3792,9 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
 
       Debug("arith::conflict") << "unate arith conflict" << endl;
     }
-  }else{
+  }
+  else
+  {
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
     d_currentPropagationList.clear();
   }
@@ -4109,16 +4114,21 @@ bool TheoryArithPrivate::isExtfReduced(int effort, Node n, Node on,
 
 void TheoryArithPrivate::propagate(Theory::Effort e) {
   // This uses model values for safety. Disable for now.
-  if(d_qflraStatus == Result::SAT &&
-     (options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
-      options::arithPropagationMode() == BOTH_PROP)
-     && hasAnyUpdates()){
+  if (d_qflraStatus == Result::SAT
+      && (options::arithPropagationMode()
+              == options::ArithPropagationMode::BOUND_INFERENCE_PROP
+          || options::arithPropagationMode()
+                 == options::ArithPropagationMode::BOTH_PROP)
+      && hasAnyUpdates())
+  {
     if(options::newProp()){
       propagateCandidatesNew();
     }else{
       propagateCandidates();
     }
-  }else{
+  }
+  else
+  {
     clearUpdates();
   }
 
@@ -4474,19 +4484,18 @@ void TheoryArithPrivate::presolve(){
   vector<Node> lemmas;
   if(!options::incrementalSolving()) {
     switch(options::arithUnateLemmaMode()){
-    case NO_PRESOLVE_LEMMAS:
-      break;
-    case INEQUALITY_PRESOLVE_LEMMAS:
-      d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
-      break;
-    case EQUALITY_PRESOLVE_LEMMAS:
-      d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
-      break;
-    case ALL_PRESOLVE_LEMMAS:
-      d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
-      d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
-      break;
-    default: Unhandled() << options::arithUnateLemmaMode();
+      case options::ArithUnateLemmaMode::NO: break;
+      case options::ArithUnateLemmaMode::INEQUALITY:
+        d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+        break;
+      case options::ArithUnateLemmaMode::EQUALITY:
+        d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+        break;
+      case options::ArithUnateLemmaMode::ALL:
+        d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+        d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+        break;
+      default: Unhandled() << options::arithUnateLemmaMode();
     }
   }
 
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index d9de9731a..d3aeb5c37 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -88,7 +88,7 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions,
   }
 
   // if we are using the eager solver reverse the abstraction
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
     if (d_funcToSignature.size() == 0)
     {
@@ -1081,7 +1081,8 @@ bool AbstractionModule::isLemmaAtom(TNode node) const {
 }
 
 void AbstractionModule::addInputAtom(TNode atom) {
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY) {
+  if (options::bitblastMode() == options::BitblastMode::LAZY)
+  {
     d_inputAtoms.insert(atom);
   }
 }
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 9d43355cc..cd906769d 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -42,7 +42,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
   prop::SatSolver *solver = nullptr;
   switch (options::bvSatSolver())
   {
-    case SAT_SOLVER_MINISAT:
+    case options::SatSolverMode::MINISAT:
     {
       prop::BVSatSolverInterface* minisat =
           prop::SatSolverFactory::createMinisat(
@@ -52,11 +52,11 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c)
       solver = minisat;
       break;
     }
-    case SAT_SOLVER_CADICAL:
+    case options::SatSolverMode::CADICAL:
       solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
                                                      "EagerBitblaster");
       break;
-    case SAT_SOLVER_CRYPTOMINISAT:
+    case options::SatSolverMode::CRYPTOMINISAT:
       solver = prop::SatSolverFactory::createCryptoMinisat(
           smtStatisticsRegistry(), "EagerBitblaster");
       break;
@@ -120,7 +120,7 @@ void EagerBitblaster::bbAtom(TNode node)
   Node atom_definition =
       NodeManager::currentNM()->mkNode(kind::EQUAL, node, atom_bb);
 
-  AlwaysAssert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
+  AlwaysAssert(options::bitblastMode() == options::BitblastMode::EAGER);
   storeBBAtom(node, atom_bb);
   d_cnfStream->convertAndAssert(
       atom_definition, false, false, RULE_INVALID, TNode::null());
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 6f8804042..14753deec 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -253,7 +253,7 @@ AlgebraicSolver::~AlgebraicSolver() {}
 
 bool AlgebraicSolver::check(Theory::Effort e)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
 
   if (!Theory::fullEffort(e)) { return true; }
   if (!useHeuristic()) { return true; }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 94dfdee14..25fe7002e 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -120,7 +120,7 @@ void BitblastSolver::bitblastQueue() {
 bool BitblastSolver::check(Theory::Effort e)
 {
   Debug("bv-bitblast") << "BitblastSolver::check (" << e << ")\n";
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
 
   ++(d_statistics.d_numCallstoCheck);
 
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 0ffd58d5a..e1732625e 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -536,10 +536,14 @@ bool Slicer::isCoreTerm(TNode node) {
   if (d_coreTermCache.find(node) == d_coreTermCache.end()) {
     Kind kind = node.getKind();
     bool not_core;
-    if (options::bitvectorEqualitySlicer() != BITVECTOR_SLICER_OFF) {
-      not_core = (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT); 
-    } else {
-      not_core = true; 
+    if (options::bitvectorEqualitySlicer() != options::BvSlicerMode::OFF)
+    {
+      not_core =
+          (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT);
+    }
+    else
+    {
+      not_core = true;
     }
     if (not_core &&
         kind != kind::EQUAL &&
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 23ffabcd1..afd99647b 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -77,7 +77,8 @@ TheoryBV::TheoryBV(context::Context* c,
   setupExtTheory();
   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     d_eagerSolver.reset(new EagerBitblastSolver(c, this));
     return;
   }
@@ -112,7 +113,8 @@ TheoryBV::TheoryBV(context::Context* c,
 TheoryBV::~TheoryBV() {}
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     return;
   }
   if (options::bitvectorEqualitySolver()) {
@@ -237,7 +239,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
   d_calledPreregister = true;
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
-  if (options::bitblastMode() == BITBLAST_MODE_EAGER)
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
     // the aig bit-blaster option is set heuristically
     // if bv abstraction is used
@@ -325,7 +327,8 @@ void TheoryBV::check(Effort e)
   // we may be getting new assertions so the model cache may not be sound
   d_invalidateModelCache.set(true);
   // if we are using the eager solver
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     // this can only happen on an empty benchmark
     if (!d_eagerSolver->isInitialized()) {
       d_eagerSolver->initialize();
@@ -354,7 +357,6 @@ void TheoryBV::check(Effort e)
     return;
   }
 
-
   if (Theory::fullEffort(e)) {
     ++(d_statistics.d_numCallsToCheckFullEffort);
   } else {
@@ -521,7 +523,8 @@ bool TheoryBV::needsCheckLastEffort() {
 bool TheoryBV::collectModelInfo(TheoryModel* m)
 {
   Assert(!inConflict());
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     if (!d_eagerSolver->collectModelInfo(m, true))
     {
       return false;
@@ -547,7 +550,8 @@ Node TheoryBV::getModelValue(TNode var) {
 
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     return;
   }
 
@@ -910,9 +914,9 @@ void TheoryBV::addSharedTerm(TNode t) {
 
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
     return EQUALITY_UNKNOWN;
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
@@ -975,9 +979,9 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 
 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
   bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
-  if (changed &&
-      options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
-      options::bitvectorAig()) {
+  if (changed && options::bitblastMode() == options::BitblastMode::EAGER
+      && options::bitvectorAig())
+  {
     // disable AIG mode
     AlwaysAssert(!d_eagerSolver->isInitialized());
     d_eagerSolver->turnOffAig();
@@ -988,9 +992,12 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
 
 void TheoryBV::setProofLog(proof::BitVectorProof* bvp)
 {
-  if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     d_eagerSolver->setProofLog(bvp);
-  }else{
+  }
+  else
+  {
     for( unsigned i=0; i< d_subtheories.size(); i++ ){
       d_subtheories[i]->setProofLog( bvp );
     }
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index c0df9f35c..765541150 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -18,6 +18,7 @@
 
 #include <vector>
 
+#include "options/theory_options.h"
 #include "theory/theory.h"
 
 namespace CVC4 {
@@ -156,7 +157,7 @@ static bool isCoreEqTerm(bool iseq, TNode term, TNodeBoolMap& cache)
       continue;
     }
 
-    if (theory::Theory::theoryOf(theory::THEORY_OF_TERM_BASED, n)
+    if (theory::Theory::theoryOf(options::TheoryOfMode::THEORY_OF_TERM_BASED, n)
         == theory::THEORY_BV)
     {
       Kind k = n.getKind();
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 42fb5cd07..890b8b2b9 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -107,7 +107,8 @@ void SygusExtension::assertFact( Node n, bool polarity, std::vector< Node >& lem
     Node m = n[0];
     Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl;
     registerMeasureTerm( m );
-    if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){
+    if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
+    {
       std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
           d_szinfo.find(m);
       Assert(its != d_szinfo.end());
@@ -245,8 +246,9 @@ void SygusExtension::assertTesterInternal( int tindex, TNode n, Node exp, std::v
       d_szinfo.find(m);
   Assert(itsz != d_szinfo.end());
   unsigned ssz = itsz->second->d_curr_search_size;
-  
-  if( options::sygusFair()==SYGUS_FAIR_DIRECT ){
+
+  if (options::sygusFair() == options::SygusFairMode::DIRECT)
+  {
     if( dt[tindex].getNumArgs()>0 ){
       quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn);
       // consider lower bounds for size of types
@@ -596,7 +598,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
   {
     Trace("sygus-sb-simple-debug") << "  Size..." << std::endl;
     // fairness
-    if (options::sygusFair() == SYGUS_FAIR_DT_SIZE && !isAnyConstant)
+    if (options::sygusFair() == options::SygusFairMode::DT_SIZE
+        && !isAnyConstant)
     {
       Node szl = nm->mkNode(DT_SIZE, n);
       Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex));
@@ -1335,7 +1338,7 @@ void SygusExtension::registerSizeTerm(Node e, std::vector<Node>& lemmas)
   d_szinfo[m]->d_anchors.push_back(e);
   d_anchor_to_measure_term[e] = m;
   NodeManager* nm = NodeManager::currentNM();
-  if (options::sygusFair() == SYGUS_FAIR_DT_SIZE)
+  if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
   {
     // update constraints on the measure term
     Node slem;
@@ -1575,7 +1578,8 @@ void SygusExtension::check( std::vector< Node >& lemmas ) {
       {
         isExc = false;
         //debugging : ensure fairness was properly handled
-        if( options::sygusFair()==SYGUS_FAIR_DT_SIZE ){  
+        if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
+        {
           Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog );
           Node prog_szv = d_td->getValuation().getModel()->getValue( prog_sz );
           Node progv_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, progv );
@@ -1768,7 +1772,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
 
 Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
 {
-  if (options::sygusFair() == SYGUS_FAIR_NONE)
+  if (options::sygusFair() == options::SygusFairMode::NONE)
   {
     return Node::null();
   }
diff --git a/src/theory/datatypes/sygus_extension.h b/src/theory/datatypes/sygus_extension.h
index 631f11040..5f6cfa00c 100644
--- a/src/theory/datatypes/sygus_extension.h
+++ b/src/theory/datatypes/sygus_extension.h
@@ -304,7 +304,7 @@ private:
    * lemmas on getSimpleSymBreakPred, see function below),
    * (3) conjecture-specific symmetry breaking lemmas, see
    * SynthConjecture::getSymmetryBreakingPredicate,
-   * (4) fairness conflicts if sygusFair() is SYGUS_FAIR_DIRECT, e.g.:
+   * (4) fairness conflicts if sygusFair() is SygusFairMode::DIRECT, e.g.:
    *    size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 )
    * where C1 and C2 are non-nullary constructors.
    */
@@ -584,12 +584,10 @@ private:
      * The measure value is an integer variable v that is a (symbolic) integer
      * value that is constrained to be less than or equal to the current search
      * size. For example, if we are using the fairness strategy
-     * SYGUS_FAIR_DT_SIZE (see options/datatype_options.h), then we constrain:
-     *   (DT_SYGUS_BOUND m n) <=> (v <= n)
-     * for all asserted fairness literals. Then, if we are enforcing fairness
-     * based on the maximum size, we assert:
-     *   (DT_SIZE e) <= v
-     * for all enumerators e.
+     * SygusFairMode::DT_SIZE (see options/datatype_options.h), then we
+     * constrain: (DT_SYGUS_BOUND m n) <=> (v <= n) for all asserted fairness
+     * literals. Then, if we are enforcing fairness based on the maximum size,
+     * we assert: (DT_SIZE e) <= v for all enumerators e.
      */
     Node getOrMkMeasureValue(std::vector<Node>& lemmas);
     /** get or make the active measure value
@@ -597,7 +595,7 @@ private:
      * The active measure value av is an integer variable that corresponds to
      * the (symbolic) value of the sum of enumerators that are yet to be
      * registered. This is to enforce the "sum of measures" strategy. For
-     * example, if we are using the fairness strategy SYGUS_FAIR_DT_SIZE,
+     * example, if we are using the fairness strategy SygusFairMode::DT_SIZE,
      * then initially av is equal to the measure value v, and the constraints
      *   (DT_SYGUS_BOUND m n) <=> (v <= n)
      * are added as before. When an enumerator e is registered, we add the
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index c7aaf572c..59e9aedcb 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -153,7 +153,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
   {
     return Node::null();
   }
-  else if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_KEEP
+  else if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::KEEP
            || (pol && k == EQUAL))
   {
     return lit;
@@ -172,7 +172,7 @@ Node BvInstantiator::hasProcessAssertion(CegInstantiator* ci,
   Trace("cegqi-bv") << "   " << sm << " <> " << tm << std::endl;
 
   Node ret;
-  if (options::cbqiBvIneqMode() == CBQI_BV_INEQ_EQ_SLACK)
+  if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK)
   {
     // if using slack, we convert constraints to a positive equality based on
     // the current model M, e.g.:
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 3420f282d..40216f7c9 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -85,14 +85,17 @@ int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
   if( e==0 ){
     return STATUS_UNFINISHED;
   }else{
-    int peffort = d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ? 2 : 1;
+    int peffort =
+        d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT ? 2
+                                                                            : 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
     }else if( e==peffort ){
       d_counter[f]++;
 
       Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
-      if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT  ){
+      if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+      {
         for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
           Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], true, Trigger::TR_RETURN_NULL );
           if( t ){
@@ -142,9 +145,12 @@ void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
   if( usable ){
     Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
     //check match option
-    if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
+    if (d_quantEngine->getInstUserPatMode() == options::UserPatMode::RESORT)
+    {
       d_user_gen_wait[q].push_back( nodes );
-    }else{
+    }
+    else
+    {
       Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW );
       if( t ){
         d_user_gen[q].push_back( t );
@@ -187,11 +193,17 @@ void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort
 }
 
 int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
-  UserPatMode upMode = d_quantEngine->getInstUserPatMode();
-  if( hasUserPatterns( f ) && upMode==USER_PAT_MODE_TRUST ){
+  options::UserPatMode upMode = d_quantEngine->getInstUserPatMode();
+  if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
+  {
     return STATUS_UNKNOWN;
-  }else{
-    int peffort = ( hasUserPatterns( f ) && upMode!=USER_PAT_MODE_IGNORE && upMode!=USER_PAT_MODE_RESORT ) ? 2 : 1;
+  }
+  else
+  {
+    int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
+                   && upMode != options::UserPatMode::RESORT)
+                      ? 2
+                      : 1;
     if( e<peffort ){
       return STATUS_UNFINISHED;
     }else{
@@ -219,17 +231,22 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
       //  d_processed_trigger.clear();
       //  d_quantEngine->getEqualityQuery()->setLiberal( true );
       //}
-      if( options::triggerActiveSelMode()!=TRIGGER_ACTIVE_SEL_ALL ){
+      if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL)
+      {
         int max_score = -1;
         Trigger * max_trigger = NULL;
         for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[0][f].begin(); itt != d_auto_gen_trigger[0][f].end(); ++itt ){
           int score = itt->first->getActiveScore();
-          if( options::triggerActiveSelMode()==TRIGGER_ACTIVE_SEL_MIN ){
+          if (options::triggerActiveSelMode()
+              == options::TriggerActiveSelMode::MIN)
+          {
             if( score>=0 && ( score<max_score || max_score<0 ) ){
               max_score = score;
               max_trigger = itt->first;
-            } 
-          }else{
+            }
+          }
+          else
+          {
             if( score>max_score ){
               max_score = score;
               max_trigger = itt->first;
@@ -241,7 +258,7 @@ int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e )
           d_auto_gen_trigger[0][f][max_trigger] = true;
         }
       }
-      
+
       bool hasInst = false;
       for( unsigned r=0; r<2; r++ ){
         for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){
@@ -374,20 +391,28 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
           }else{
             Assert(Trigger::isAtomicTrigger(pat));
             if( pat.getType().isBoolean() && rpoleq.isNull() ){
-              if( options::literalMatchMode()==LITERAL_MATCH_USE ){
+              if (options::literalMatchMode() == options::LiteralMatchMode::USE)
+              {
                 pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
-              }else if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+              }
+              else if (options::literalMatchMode()
+                       != options::LiteralMatchMode::NONE)
+              {
                 pat = NodeManager::currentNM()->mkNode( EQUAL, pat, NodeManager::currentNM()->mkConst( rpol==1 ) );
               }
             }else{
               Assert(!rpoleq.isNull());
               if( rpol==-1 ){
-                if( options::literalMatchMode()!=LITERAL_MATCH_NONE ){
+                if (options::literalMatchMode()
+                    != options::LiteralMatchMode::NONE)
+                {
                   //all equivalence classes except rpoleq
                   pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
                 }
               }else if( rpol==1 ){
-                if( options::literalMatchMode()==LITERAL_MATCH_AGG ){
+                if (options::literalMatchMode()
+                    == options::LiteralMatchMode::AGG)
+                {
                   //only equivalence class rpoleq
                   pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq );
                 }
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 1a014939f..052bc910c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -54,63 +54,67 @@ public:
   std::string identify() const override { return std::string("UserPatterns"); }
 };/* class InstStrategyUserPatterns */
 
-class InstStrategyAutoGenTriggers : public InstStrategy {
-public:
-  enum {
+class InstStrategyAutoGenTriggers : public InstStrategy
+{
+ public:
+  enum
+  {
     RELEVANCE_NONE,
     RELEVANCE_DEFAULT,
   };
-private:
+
+ private:
   /** trigger generation strategy */
-  TriggerSelMode d_tr_strategy;
+  options::TriggerSelMode d_tr_strategy;
   /** regeneration */
   bool d_regenerate;
   int d_regenerate_frequency;
   /** (single,multi) triggers for each quantifier */
-  std::map< Node, std::map< inst::Trigger*, bool > > d_auto_gen_trigger[2];
-  std::map< Node, int > d_counter;
+  std::map<Node, std::map<inst::Trigger*, bool> > d_auto_gen_trigger[2];
+  std::map<Node, int> d_counter;
   /** single, multi triggers for each quantifier */
-  std::map< Node, std::vector< Node > > d_patTerms[2];
-  std::map< Node, std::map< Node, bool > > d_patReqPol;
+  std::map<Node, std::vector<Node> > d_patTerms[2];
+  std::map<Node, std::map<Node, bool> > d_patReqPol;
   /** information about triggers */
-  std::map< Node, bool > d_is_single_trigger;
-  std::map< Node, bool > d_single_trigger_gen;
-  std::map< Node, bool > d_made_multi_trigger;
-  //processed trigger this round
-  std::map< Node, std::map< inst::Trigger*, bool > > d_processed_trigger;
-  //instantiation no patterns
-  std::map< Node, std::vector< Node > > d_user_no_gen;
+  std::map<Node, bool> d_is_single_trigger;
+  std::map<Node, bool> d_single_trigger_gen;
+  std::map<Node, bool> d_made_multi_trigger;
+  // processed trigger this round
+  std::map<Node, std::map<inst::Trigger*, bool> > d_processed_trigger;
+  // instantiation no patterns
+  std::map<Node, std::vector<Node> > d_user_no_gen;
   // number of trigger variables per quantifier
-  std::map< Node, unsigned > d_num_trigger_vars;
-  std::map< Node, Node > d_vc_partition[2];
-  std::map< Node, Node > d_pat_to_mpat;
-private:
+  std::map<Node, unsigned> d_num_trigger_vars;
+  std::map<Node, Node> d_vc_partition[2];
+  std::map<Node, Node> d_pat_to_mpat;
+
+ private:
   /** process functions */
- void processResetInstantiationRound(Theory::Effort effort) override;
- int process(Node q, Theory::Effort effort, int e) override;
- /** generate triggers */
- void generateTriggers(Node q);
- void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
- void addTrigger(inst::Trigger* tr, Node f);
- /** has user patterns */
- bool hasUserPatterns(Node q);
- /** has user patterns */
- std::map<Node, bool> d_hasUserPatterns;
+  void processResetInstantiationRound(Theory::Effort effort) override;
+  int process(Node q, Theory::Effort effort, int e) override;
+  /** generate triggers */
+  void generateTriggers(Node q);
+  void addPatternToPool(Node q, Node pat, unsigned num_fv, Node mpat);
+  void addTrigger(inst::Trigger* tr, Node f);
+  /** has user patterns */
+  bool hasUserPatterns(Node q);
+  /** has user patterns */
+  std::map<Node, bool> d_hasUserPatterns;
 
-public:
- InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
- ~InstStrategyAutoGenTriggers() {}
+ public:
+  InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantRelevance* qr);
+  ~InstStrategyAutoGenTriggers() {}
 
-public:
+ public:
   /** get auto-generated trigger */
-  inst::Trigger* getAutoGenTrigger( Node q );
+  inst::Trigger* getAutoGenTrigger(Node q);
   /** identify */
   std::string identify() const override
   {
     return std::string("AutoGenTriggers");
   }
   /** add pattern */
-  void addUserNoPattern( Node q, Node pat );
+  void addUserNoPattern(Node q, Node pat);
 
  private:
   /**
@@ -118,9 +122,7 @@ public:
    * owned by the instantiation engine that owns this class.
    */
   QuantRelevance* d_quant_rel;
-};/* class InstStrategyAutoGenTriggers */
-
-
+}; /* class InstStrategyAutoGenTriggers */
 }
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 23b1ff6c9..b91a9ba63 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -46,7 +46,8 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe)
   if (options::eMatching()) {
     // these are the instantiation strategies for E-matching
     // user-provided patterns
-    if (options::userPatternsQuant() != USER_PAT_MODE_IGNORE) {
+    if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
+    {
       d_isup.reset(new InstStrategyUserPatterns(d_quantEngine));
       d_instStrategies.push_back(d_isup.get());
     }
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index f539bccf5..e177e24a6 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -429,9 +429,19 @@ bool Trigger::isSimpleTrigger( Node n ){
 }
 
 //store triggers in reqPol, indicating their polarity (if any) they must appear to falsify the quantified formula
-void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
-                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable ){
+void Trigger::collectPatTerms2(Node q,
+                               Node n,
+                               std::map<Node, std::vector<Node> >& visited,
+                               std::map<Node, TriggerTermInfo>& tinfo,
+                               options::TriggerSelMode tstrt,
+                               std::vector<Node>& exclude,
+                               std::vector<Node>& added,
+                               bool pol,
+                               bool hasPol,
+                               bool epol,
+                               bool hasEPol,
+                               bool knowIsUsable)
+{
   std::map< Node, std::vector< Node > >::iterator itv = visited.find( n );
   if( itv==visited.end() ){
     visited[ n ].clear();
@@ -488,7 +498,10 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
           Assert(added2[i] != nu);
           // if child was not already removed
           if( tinfo.find( added2[i] )!=tinfo.end() ){
-            if( tstrt==quantifiers::TRIGGER_SEL_MAX || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_MAX && !nu_single ) ){
+            if (tstrt == options::TriggerSelMode::MAX
+                || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX
+                    && !nu_single))
+            {
               // discard all subterms
               // do not remove if it has smaller weight
               if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
@@ -498,7 +511,9 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
                 visited[added2[i]].clear();
                 tinfo.erase(added2[i]);
               }
-            }else{
+            }
+            else
+            {
               if( tinfo[ nu ].d_fv.size()==tinfo[ added2[i] ].d_fv.size() ){
                 if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
                 {
@@ -516,9 +531,15 @@ void Trigger::collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Nod
             }
           }
         }
-        if( rm_nu && ( tstrt==quantifiers::TRIGGER_SEL_MIN || ( tstrt==quantifiers::TRIGGER_SEL_MIN_SINGLE_ALL && nu_single ) ) ){
+        if (rm_nu
+            && (tstrt == options::TriggerSelMode::MIN
+                || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL
+                    && nu_single)))
+        {
           tinfo.erase( nu );
-        }else{
+        }
+        else
+        {
           if( std::find( added.begin(), added.end(), nu )==added.end() ){
             added.push_back( nu );
           }
@@ -593,14 +614,21 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector<
   return true;
 }
 
-void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, 
-                               std::map< Node, TriggerTermInfo >& tinfo, bool filterInst ){
+void Trigger::collectPatTerms(Node q,
+                              Node n,
+                              std::vector<Node>& patTerms,
+                              options::TriggerSelMode tstrt,
+                              std::vector<Node>& exclude,
+                              std::map<Node, TriggerTermInfo>& tinfo,
+                              bool filterInst)
+{
   std::map< Node, std::vector< Node > > visited;
   if( filterInst ){
     //immediately do not consider any term t for which another term is an instance of t
     std::vector< Node > patTerms2;
     std::map< Node, TriggerTermInfo > tinfo2;
-    collectPatTerms( q, n, patTerms2, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo2, false );
+    collectPatTerms(
+        q, n, patTerms2, options::TriggerSelMode::ALL, exclude, tinfo2, false);
     std::vector< Node > temp;
     temp.insert( temp.begin(), patTerms2.begin(), patTerms2.end() );
     filterTriggerInstances(temp);
@@ -623,7 +651,8 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
         Trace("trigger-filter-instance") << std::endl;
       }
     }
-    if( tstrt==quantifiers::TRIGGER_SEL_ALL ){
+    if (tstrt == options::TriggerSelMode::ALL)
+    {
       for( unsigned i=0; i<temp.size(); i++ ){
         //copy information
         tinfo[temp[i]].d_fv.insert( tinfo[temp[i]].d_fv.end(), tinfo2[temp[i]].d_fv.begin(), tinfo2[temp[i]].d_fv.end() );
@@ -632,7 +661,9 @@ void Trigger::collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, qu
         patTerms.push_back( temp[i] );
       }
       return;
-    }else{
+    }
+    else
+    {
       //do not consider terms that have instances
       for( unsigned i=0; i<patTerms2.size(); i++ ){
         if( std::find( temp.begin(), temp.end(), patTerms2[i] )==temp.end() ){
@@ -875,7 +906,7 @@ void Trigger::getTriggerVariables(Node n, Node q, std::vector<Node>& t_vars)
   std::map< Node, TriggerTermInfo > tinfo;
   // collect all patterns from n
   std::vector< Node > exclude;
-  collectPatTerms(q, n, patTerms, quantifiers::TRIGGER_SEL_ALL, exclude, tinfo);
+  collectPatTerms(q, n, patTerms, options::TriggerSelMode::ALL, exclude, tinfo);
   //collect all variables from all patterns in patTerms, add to t_vars
   for (const Node& pat : patTerms)
   {
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index d47ea72ee..e955543db 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -273,9 +273,13 @@ class Trigger {
    *     in the vector we are returning, e.g. we do not return f( x ) if we are
    *     also returning f( f( x ) ). TODO: revisit this (issue #1211)
    */
-  static void collectPatTerms( Node q, Node n, std::vector< Node >& patTerms, quantifiers::TriggerSelMode tstrt,
-                               std::vector< Node >& exclude, std::map< Node, TriggerTermInfo >& tinfo,
-                               bool filterInst = false );
+  static void collectPatTerms(Node q,
+                              Node n,
+                              std::vector<Node>& patTerms,
+                              options::TriggerSelMode tstrt,
+                              std::vector<Node>& exclude,
+                              std::map<Node, TriggerTermInfo>& tinfo,
+                              bool filterInst = false);
 
   /** Is n a usable trigger in quantified formula q?
    *
@@ -380,9 +384,18 @@ class Trigger {
    *
    * We add the triggers we collected recursively in n into added.
    */
-  static void collectPatTerms2( Node q, Node n, std::map< Node, std::vector< Node > >& visited, std::map< Node, TriggerTermInfo >& tinfo, 
-                                quantifiers::TriggerSelMode tstrt, std::vector< Node >& exclude, std::vector< Node >& added,
-                                bool pol, bool hasPol, bool epol, bool hasEPol, bool knowIsUsable = false );
+  static void collectPatTerms2(Node q,
+                               Node n,
+                               std::map<Node, std::vector<Node> >& visited,
+                               std::map<Node, TriggerTermInfo>& tinfo,
+                               options::TriggerSelMode tstrt,
+                               std::vector<Node>& exclude,
+                               std::vector<Node>& added,
+                               bool pol,
+                               bool hasPol,
+                               bool epol,
+                               bool hasEPol,
+                               bool knowIsUsable = false);
 
   /** filter all nodes that have trigger instances
    *
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index f7fd13d4d..f72a0d1b4 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -111,9 +111,12 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
       }
     }
   }
-  if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_EE ){
+  if (options::quantRepMode() == options::QuantRepMode::EE)
+  {
     return r;
-  }else{
+  }
+  else
+  {
     TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
     std::map<Node, Node>& v_int_rep = d_int_rep[v_tn];
     std::map<Node, Node>::const_iterator itir = v_int_rep.find(r);
@@ -239,11 +242,14 @@ int EqualityQueryQuantifiersEngine::getRepScore(Node n,
       return options::instLevelInputOnly() ? -1 : 0;
     }
   }else{
-    if( options::quantRepMode()==quantifiers::QUANT_REP_MODE_FIRST ){
+    if (options::quantRepMode() == options::QuantRepMode::FIRST)
+    {
       //score prefers earliest use of this term as a representative
       return d_rep_score.find( n )==d_rep_score.end() ? -1 : d_rep_score[n];
-    }else{
-      Assert(options::quantRepMode() == quantifiers::QUANT_REP_MODE_DEPTH);
+    }
+    else
+    {
+      Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
       return quantifiers::TermUtil::getTermDepth( n );
     }
   }
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index d6c939e5d..206c8f9dd 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -603,12 +603,15 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
         d_quant_cond[f] = op;
       }
 
-      if( options::mbqiMode()==MBQI_NONE ){
+      if (options::mbqiMode() == options::MbqiMode::NONE)
+      {
         //just exhaustive instantiate
         Node c = mkCondDefault( fmfmc, f );
         d_quant_models[f].addEntry( fmfmc, c, d_false );
         return exhaustiveInstantiate( fmfmc, f, c, -1);
-      }else{
+      }
+      else
+      {
         //model check the quantifier
         doCheck(fmfmc, f, d_quant_models[f], f[1]);
         Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index caca25fde..a6e1a369c 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -37,7 +37,7 @@ QModelBuilder::QModelBuilder(context::Context* c, QuantifiersEngine* qe)
       d_triedLemmas(0) {}
 
 bool QModelBuilder::optUseModel() {
-  return options::mbqiMode()!=MBQI_NONE || options::fmfBound();
+  return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound();
 }
 
 bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index cdaaa239a..5b2931e42 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -219,9 +219,9 @@ int ModelEngine::checkModel(){
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   // FMC uses two sub-effort levels
-  int e_max = options::mbqiMode() == MBQI_FMC
+  int e_max = options::mbqiMode() == options::MbqiMode::FMC
                   ? 2
-                  : (options::mbqiMode() == MBQI_TRUST ? 0 : 1);
+                  : (options::mbqiMode() == options::MbqiMode::TRUST ? 0 : 1);
   for( int e=0; e<e_max; e++) {
     d_incomplete_quants.clear();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index de46eee74..89f4f2989 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -17,6 +17,7 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "options/theory_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -652,7 +653,9 @@ bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
     }
     //check if it is entailed
     Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
-    std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
+    std::pair<bool, Node> et =
+        p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(
+            options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew);
     ++(p->d_statistics.d_entailment_checks);
     Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
     if( !et.first ){
@@ -1901,11 +1904,11 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) {
   bool performCheck = false;
   if( options::quantConflictFind() && !d_conflict ){
     if( level==Theory::EFFORT_LAST_CALL ){
-      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_LAST_CALL;
+      performCheck = options::qcfWhenMode() == options::QcfWhenMode::LAST_CALL;
     }else if( level==Theory::EFFORT_FULL ){
-      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_DEFAULT;
+      performCheck = options::qcfWhenMode() == options::QcfWhenMode::DEFAULT;
     }else if( level==Theory::EFFORT_STANDARD ){
-      performCheck = options::qcfWhenMode()==QCF_WHEN_MODE_STD;
+      performCheck = options::qcfWhenMode() == options::QcfWhenMode::STD;
     }
   }
   return performCheck;
@@ -1956,8 +1959,9 @@ inline QuantConflictFind::Effort QcfEffortStart() {
 // Returns the beginning of a range of efforts. The value returned is included
 // in the range.
 inline QuantConflictFind::Effort QcfEffortEnd() {
-  return options::qcfMode() == QCF_PROP_EQ ? QuantConflictFind::EFFORT_PROP_EQ
-                                           : QuantConflictFind::EFFORT_CONFLICT;
+  return options::qcfMode() == options::QcfMode::PROP_EQ
+             ? QuantConflictFind::EFFORT_PROP_EQ
+             : QuantConflictFind::EFFORT_CONFLICT;
 }
 
 }  // namespace
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 32bd2b0e8..5ad01009a 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -54,11 +54,16 @@ void QuantDSplit::checkOwnership(Node q)
       }
       else
       {
-        if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
+        if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG)
+        {
           // split if it is a finite datatype
           doSplit = dt.isInterpretedFinite(tn);
-        }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
-          if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){
+        }
+        else if (options::quantDynamicSplit()
+                 == options::QuantDSplitMode::DEFAULT)
+        {
+          if (!d_quantEngine->isFiniteBound(q, q[0][i]))
+          {
             if (dt.isInterpretedFinite(tn))
             {
               // split if goes from being unhandled -> handled by finite
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 8d65523e1..d5bee4916 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -658,12 +658,15 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
     return iti->second;
   }else{
     Node prev = ret;
-    if( ret.getKind()==EQUAL && options::iteLiftQuant()!=ITE_LIFT_QUANT_MODE_NONE ){
+    if (ret.getKind() == EQUAL
+        && options::iteLiftQuant() != options::IteLiftQuantMode::NONE)
+    {
       for( size_t i=0; i<2; i++ ){
         if( ret[i].getKind()==ITE ){
           Node no = i==0 ? ret[1] : ret[0];
           if( no.getKind()!=ITE ){
-            bool doRewrite = options::iteLiftQuant()==ITE_LIFT_QUANT_MODE_ALL;
+            bool doRewrite =
+                options::iteLiftQuant() == options::IteLiftQuantMode::ALL;
             std::vector< Node > children;
             children.push_back( ret[i][0] );
             for( size_t j=1; j<=2; j++ ){
@@ -1545,7 +1548,10 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns
   }
   if( containsQuantifiers( n ) ){
     Node ret = n;
-    if( topLevel && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL && ( n.getKind()==AND || ( n.getKind()==NOT && n[0].getKind()==OR ) ) ){
+    if (topLevel
+        && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
+        && (n.getKind() == AND || (n.getKind() == NOT && n[0].getKind() == OR)))
+    {
       std::vector< Node > children;
       Node nc = n.getKind()==NOT ? n[0] : n;
       for( unsigned i=0; i<nc.getNumChildren(); i++ ){
@@ -1556,25 +1562,33 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns
         children.push_back( ncc );
       }
       ret = NodeManager::currentNM()->mkNode( AND, children );
-    }else if( n.getKind()==NOT ){
+    }
+    else if (n.getKind() == NOT)
+    {
       ret = computePrenexAgg( n[0], false, visited ).negate();
-    }else if( n.getKind()==FORALL ){
-    /*
-      Node nn = computePrenexAgg( n[1], false );
-      if( nn!=n[1] ){
-        if( n.getNumChildren()==2 ){
-          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn );
-        }else{
-          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] );
+    }
+    else if (n.getKind() == FORALL)
+    {
+      /*
+        Node nn = computePrenexAgg( n[1], false );
+        if( nn!=n[1] ){
+          if( n.getNumChildren()==2 ){
+            return NodeManager::currentNM()->mkNode( FORALL, n[0], nn );
+          }else{
+            return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] );
+          }
         }
-      }
-      */
+        */
       std::vector< Node > children;
-      if( n[1].getKind()==OR && options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL ){
+      if (n[1].getKind() == OR
+          && options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL)
+      {
         for( unsigned i=0; i<n[1].getNumChildren(); i++ ){
           children.push_back( computePrenexAgg( n[1][i], false, visited ) );
         }
-      }else{
+      }
+      else
+      {
         children.push_back( computePrenexAgg( n[1], false, visited ) );
       }
       std::vector< Node > args;
@@ -1600,7 +1614,9 @@ Node QuantifiersRewriter::computePrenexAgg( Node n, bool topLevel, std::map< uns
       } 
       Node nb = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
       ret = mkForall( args, nb, iplc, true );
-    }else{
+    }
+    else
+    {
       std::vector< Node > args;
       std::vector< Node > nargs;
       Node nn = computePrenex( n, args, nargs, true, true );
@@ -1949,7 +1965,9 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg
 }
 
 bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){
-  bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST;
+  bool is_strict_trigger =
+      qa.d_hasPattern
+      && options::userPatternsQuant() == options::UserPatMode::TRUST;
   bool is_std = qa.isStandard() && !is_strict_trigger;
   if (computeOption == COMPUTE_ELIM_SYMBOLS)
   {
@@ -1966,7 +1984,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
   else if (computeOption == COMPUTE_PROCESS_TERMS)
   {
     return options::condRewriteQuant() || options::elimExtArithQuant()
-           || options::iteLiftQuant() != ITE_LIFT_QUANT_MODE_NONE;
+           || options::iteLiftQuant() != options::IteLiftQuantMode::NONE;
   }
   else if (computeOption == COMPUTE_COND_SPLIT)
   {
@@ -1975,7 +1993,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
   }
   else if (computeOption == COMPUTE_PRENEX)
   {
-    return options::prenexQuant() != PRENEX_QUANT_NONE
+    return options::prenexQuant() != options::PrenexQuantMode::NONE
            && !options::aggressiveMiniscopeQuant() && is_std;
   }
   else if (computeOption == COMPUTE_VAR_ELIMINATION)
@@ -1999,7 +2017,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
     n = computeElimSymbols( n );
   }else if( computeOption==COMPUTE_MINISCOPING ){
-    if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
+    if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
+        || options::prenexQuant() == options::PrenexQuantMode::NORMAL)
+    {
       if( !qa.d_qid_num.isNull() ){
         //already processed this, return self
         return f;
@@ -2019,10 +2039,14 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   }else if( computeOption==COMPUTE_COND_SPLIT ){
     n = computeCondSplit(n, args, qa);
   }else if( computeOption==COMPUTE_PRENEX ){
-    if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
+    if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
+        || options::prenexQuant() == options::PrenexQuantMode::NORMAL)
+    {
       //will rewrite at preprocess time
       return f;
-    }else{
+    }
+    else
+    {
       std::vector< Node > nargs;
       n = computePrenex( n, args, nargs, true, false );
       Assert(nargs.empty());
@@ -2267,7 +2291,9 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
     }
   }
   //pull all quantifiers globally
-  if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
+  if (options::prenexQuant() == options::PrenexQuantMode::DISJ_NORMAL
+      || options::prenexQuant() == options::PrenexQuantMode::NORMAL)
+  {
     Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
     std::map< unsigned, std::map< Node, Node > > visited;
     n = quantifiers::QuantifiersRewriter::computePrenexAgg( n, true, visited );
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 99e7b5a8c..248128c1e 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -146,7 +146,8 @@ bool QueryGenerator::addTerm(Node n, std::ostream& out)
 void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
 {
   // external query
-  if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_ALL)
+  if (options::sygusQueryGenDumpFiles()
+      == options::SygusQueryDumpFilesMode::ALL)
   {
     dumpQuery(qy, spIndex);
   }
@@ -179,7 +180,8 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
       ss << "but CVC4 answered unsat!" << std::endl;
       AlwaysAssert(false) << ss.str();
     }
-    if (options::sygusQueryGenDumpFiles() == SYGUS_QUERY_DUMP_UNSOLVED)
+    if (options::sygusQueryGenDumpFiles()
+        == options::SygusQueryDumpFilesMode::UNSOLVED)
     {
       if (r.asSatisfiabilityResult().isSat() != Result::SAT)
       {
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 69e0ef70a..e36047e67 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -109,7 +109,7 @@ void CegSingleInv::initialize(Node q)
   {
     // We are fully single invocation, set single invocation if we haven't
     // disabled single invocation techniques.
-    if (options::cegqiSingleInvMode() != CEGQI_SI_MODE_NONE)
+    if (options::cegqiSingleInvMode() != options::CegqiSingleInvMode::NONE)
     {
       d_single_invocation = true;
       return;
@@ -118,25 +118,25 @@ void CegSingleInv::initialize(Node q)
   // We are processing without single invocation techniques, now check if
   // we should fix an invariant template (post-condition strengthening or
   // pre-condition weakening).
-  SygusInvTemplMode tmode = options::sygusInvTemplMode();
-  if (tmode != SYGUS_INV_TEMPL_MODE_NONE)
+  options::SygusInvTemplMode tmode = options::sygusInvTemplMode();
+  if (tmode != options::SygusInvTemplMode::NONE)
   {
     // currently only works for single predicate synthesis
     if (q[0].getNumChildren() > 1 || !q[0][0].getType().isPredicate())
     {
-      tmode = SYGUS_INV_TEMPL_MODE_NONE;
+      tmode = options::SygusInvTemplMode::NONE;
     }
     else if (!options::sygusInvTemplWhenSyntax())
     {
       // only use invariant templates if no syntactic restrictions
       if (CegGrammarConstructor::hasSyntaxRestrictions(q))
       {
-        tmode = SYGUS_INV_TEMPL_MODE_NONE;
+        tmode = options::SygusInvTemplMode::NONE;
       }
     }
   }
 
-  if (tmode == SYGUS_INV_TEMPL_MODE_NONE)
+  if (tmode == options::SygusInvTemplMode::NONE)
   {
     // not processing invariant templates
     return;
@@ -243,13 +243,13 @@ void CegSingleInv::initialize(Node q)
                      << std::endl;
   if (templ.isNull())
   {
-    if (tmode == SYGUS_INV_TEMPL_MODE_PRE)
+    if (tmode == options::SygusInvTemplMode::PRE)
     {
       templ = nm->mkNode(OR, d_trans_pre[prog], d_templ_arg[prog]);
     }
     else
     {
-      Assert(tmode == SYGUS_INV_TEMPL_MODE_POST);
+      Assert(tmode == options::SygusInvTemplMode::POST);
       templ = nm->mkNode(AND, d_trans_post[prog], d_templ_arg[prog]);
     }
   }
@@ -269,8 +269,11 @@ void CegSingleInv::initialize(Node q)
 void CegSingleInv::finishInit(bool syntaxRestricted)
 {
   Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl;
-  // do not do single invocation if grammar is restricted and CEGQI_SI_MODE_ALL is not enabled
-  if( options::cegqiSingleInvMode()==CEGQI_SI_MODE_USE && d_single_invocation && syntaxRestricted ){
+  // do not do single invocation if grammar is restricted and
+  // options::CegqiSingleInvMode::ALL is not enabled
+  if (options::cegqiSingleInvMode() == options::CegqiSingleInvMode::USE
+      && d_single_invocation && syntaxRestricted)
+  {
     d_single_invocation = false;
     Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
   }
@@ -551,17 +554,19 @@ Node CegSingleInv::reconstructToSyntax(Node s,
 
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
-  if (options::cegqiSingleInvReconstruct() != CEGQI_SI_RCONS_MODE_NONE
+  if (options::cegqiSingleInvReconstruct()
+          != options::CegqiSingleInvRconsMode::NONE
       && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus)
   {
     d_sol->preregisterConjecture( d_orig_conjecture );
     int enumLimit = -1;
-    if (options::cegqiSingleInvReconstruct() == CEGQI_SI_RCONS_MODE_TRY)
+    if (options::cegqiSingleInvReconstruct()
+        == options::CegqiSingleInvRconsMode::TRY)
     {
       enumLimit = 0;
     }
     else if (options::cegqiSingleInvReconstruct()
-             == CEGQI_SI_RCONS_MODE_ALL_LIMIT)
+             == options::CegqiSingleInvRconsMode::ALL_LIMIT)
     {
       enumLimit = options::cegqiSingleInvReconstructLimit();
     }
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index a4dc241b8..78ea5b22f 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -52,7 +52,7 @@ bool Cegis::initialize(Node conj,
   }
 
   // assign the cegis sampler if applicable
-  if (options::cegisSample() != CEGIS_SAMPLE_NONE)
+  if (options::cegisSample() != options::CegisSampleMode::NONE)
   {
     Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
                           << std::endl;
@@ -81,7 +81,8 @@ bool Cegis::processInitialize(Node conj,
     // grammar construction was not simple.
     bool useSymCons = false;
     if (options::sygusRepairConst()
-        || options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE)
+        || options::sygusGrammarConsMode()
+               != options::SygusGrammarConsMode::SIMPLE)
     {
       TypeNode ctn = candidates[i].getType();
       d_tds->registerSygusType(ctn);
@@ -305,7 +306,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     return false;
   }
 
-  if (options::cegisSample() != CEGIS_SAMPLE_NONE && lems.empty())
+  if (options::cegisSample() != options::CegisSampleMode::NONE && lems.empty())
   {
     // if we didn't add a lemma, trying sampling to add a refinement lemma
     // that immediately refutes the candidate we just constructed
@@ -636,7 +637,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
           Trace("cegqi-engine") << "  *** Refine by sampling" << std::endl;
           addRefinementLemma(rlem);
           // if trust, we are not interested in sending out refinement lemmas
-          if (options::cegisSample() != CEGIS_SAMPLE_TRUST)
+          if (options::cegisSample() != options::CegisSampleMode::TRUST)
           {
             Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem);
             lems.push_back(lem);
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 2bc412361..8812032ba 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -405,9 +405,9 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy(
 {
   d_initialized = false;
   d_tds = d_qe->getTermDatabaseSygus();
-  SygusUnifPiMode mode = options::sygusUnifPi();
-  d_useCondPool =
-      mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
+  options::SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool = mode == options::SygusUnifPiMode::CENUM
+                  || mode == options::SygusUnifPiMode::CENUM_IGAIN;
 }
 
 Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n)
@@ -639,7 +639,8 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   }
   Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                            << " to strategy point " << si.d_pt << "\n";
-  bool useSymCons = options::sygusGrammarConsMode() != SYGUS_GCONS_SIMPLE;
+  bool useSymCons =
+      options::sygusGrammarConsMode() != options::SygusGrammarConsMode::SIMPLE;
   d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, useSymCons);
 }
 
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 8c005bd3c..78fbc48f3 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -538,7 +538,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       itc;
   // maps types to the index of its "any term" grammar construction
   std::map<TypeNode, unsigned> typeToGAnyTerm;
-  SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
+  options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
   for (unsigned i = 0, size = types.size(); i < size; ++i)
   {
     std::stringstream ss;
@@ -571,15 +571,16 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
   {
     Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " " << unres_types[i] << std::endl;
     TypeNode unres_t = unres_types[i];
-    SygusGrammarConsMode tsgcm = sgcm;
-    if (tsgcm == SYGUS_GCONS_ANY_TERM || tsgcm == SYGUS_GCONS_ANY_TERM_CONCISE)
+    options::SygusGrammarConsMode tsgcm = sgcm;
+    if (tsgcm == options::SygusGrammarConsMode::ANY_TERM
+        || tsgcm == options::SygusGrammarConsMode::ANY_TERM_CONCISE)
     {
       // If the type does not support any term, we do any constant instead.
       // We also fall back on any constant construction if the type has no
       // constructors at this point (e.g. it simply encodes all constants).
       if (!types[i].isReal())
       {
-        tsgcm = SYGUS_GCONS_ANY_CONST;
+        tsgcm = options::SygusGrammarConsMode::ANY_CONST;
       }
       else
       {
@@ -629,7 +630,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     //add constants
     std::vector<Node> consts;
     mkSygusConstantsForType(types[i], consts);
-    if (tsgcm == SYGUS_GCONS_ANY_CONST)
+    if (tsgcm == options::SygusGrammarConsMode::ANY_CONST)
     {
       // Use the any constant constructor. Notice that for types that don't
       // have constants (e.g. uninterpreted or function types), we don't add
@@ -923,7 +924,8 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     // the references).
     const SygusDatatype& sdti = sdts[i].d_sdt;
     // whether we will use the polynomial grammar
-    bool polynomialGrammar = sgcm == SYGUS_GCONS_ANY_TERM_CONCISE;
+    bool polynomialGrammar =
+        sgcm == options::SygusGrammarConsMode::ANY_TERM_CONCISE;
     // A set of constructor indices that will be used in the overall sum we
     // are constructing; indices of constructors corresponding to builtin
     // arithmetic operators will be excluded from this set.
@@ -1198,7 +1200,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // TODO #1935 ITEs are added to Boolean grammars so that we can infer
       // unification strategies. We can do away with this if we can infer
       // unification strategies from and/or/not
-      if (k == ITE && options::sygusUnifPi() == SYGUS_UNIF_PI_NONE)
+      if (k == ITE && options::sygusUnifPi() == options::SygusUnifPiMode::NONE)
       {
         continue;
       }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 47975d4b7..2b85595cd 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -61,10 +61,10 @@ void SygusUnifRl::initializeCandidate(
     d_cand_to_hd_count[f] = 0;
   }
   // check whether we are using condition enumeration
-  SygusUnifPiMode mode = options::sygusUnifPi();
-  d_useCondPool =
-      mode == SYGUS_UNIF_PI_CENUM || mode == SYGUS_UNIF_PI_CENUM_IGAIN;
-  d_useCondPoolIGain = mode == SYGUS_UNIF_PI_CENUM_IGAIN;
+  options::SygusUnifPiMode mode = options::sygusUnifPi();
+  d_useCondPool = mode == options::SygusUnifPiMode::CENUM
+                  || mode == options::SygusUnifPiMode::CENUM_IGAIN;
+  d_useCondPoolIGain = mode == options::SygusUnifPiMode::CENUM_IGAIN;
 }
 
 void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e30f9771c..03449589b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -66,7 +66,7 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p)
   {
     d_modules.push_back(d_ceg_pbe.get());
   }
-  if (options::sygusUnifPi() != SYGUS_UNIF_PI_NONE)
+  if (options::sygusUnifPi() != options::SygusUnifPiMode::NONE)
   {
     d_modules.push_back(d_ceg_cegisUnif.get());
   }
@@ -483,7 +483,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
   bool sk_refine = (!isGround() || d_refine_count == 0) && constructed_cand;
   if (sk_refine)
   {
-    if (options::cegisSample() == CEGIS_SAMPLE_TRUST)
+    if (options::cegisSample() == options::CegisSampleMode::TRUST)
     {
       // we have that the current candidate passed a sample test
       // since we trust sampling in this mode, we assert there is no
@@ -799,14 +799,17 @@ Node SynthConjecture::getEnumeratedValue(Node e, bool& activeIncomplete)
       // or basic. The auto mode always prefers the optimized enumerator over
       // the basic one.
       Assert(d_tds->isBasicEnumerator(e));
-      if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM_BASIC)
+      if (options::sygusActiveGenMode()
+          == options::SygusActiveGenMode::ENUM_BASIC)
       {
         d_evg[e].reset(new EnumValGeneratorBasic(d_tds, e.getType()));
       }
       else
       {
-        Assert(options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_ENUM
-               || options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO);
+        Assert(options::sygusActiveGenMode()
+                   == options::SygusActiveGenMode::ENUM
+               || options::sygusActiveGenMode()
+                      == options::SygusActiveGenMode::AUTO);
         d_evg[e].reset(new SygusEnumerator(d_tds, this));
       }
     }
@@ -1061,7 +1064,8 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
 
       if (status != 0
           && (options::sygusRewSynth() || options::sygusQueryGen()
-              || options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE))
+              || options::sygusFilterSolMode()
+                     != options::SygusFilterSolMode::NONE))
       {
         Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
         std::map<Node, ExpressionMinerManager>::iterator its =
@@ -1078,13 +1082,16 @@ void SynthConjecture::printSynthSolution(std::ostream& out)
           {
             d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh());
           }
-          if (options::sygusFilterSolMode() != SYGUS_FILTER_SOL_NONE)
+          if (options::sygusFilterSolMode()
+              != options::SygusFilterSolMode::NONE)
           {
-            if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_STRONG)
+            if (options::sygusFilterSolMode()
+                == options::SygusFilterSolMode::STRONG)
             {
               d_exprm[prog].enableFilterStrongSolutions();
             }
-            else if (options::sygusFilterSolMode() == SYGUS_FILTER_SOL_WEAK)
+            else if (options::sygusFilterSolMode()
+                     == options::SygusFilterSolMode::WEAK)
             {
               d_exprm[prog].enableFilterWeakSolutions();
             }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 0279ca531..1fda55172 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -453,7 +453,7 @@ void TermDbSygus::registerEnumerator(Node e,
 
   // determine if we are actively-generated
   bool isActiveGen = false;
-  if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE)
+  if (options::sygusActiveGenMode() != options::SygusActiveGenMode::NONE)
   {
     if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
     {
@@ -481,7 +481,7 @@ void TermDbSygus::registerEnumerator(Node e,
     {
       // If the enumerator is the single function-to-synthesize, if auto is
       // enabled, we infer whether it is better to enable active generation.
-      if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO)
+      if (options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO)
       {
         // We use active generation if the grammar of the enumerator does not
         // have ITE and is not Boolean. Experimentally, it is better to
@@ -513,9 +513,9 @@ void TermDbSygus::registerEnumerator(Node e,
                     << " returned " << isActiveGen << std::endl;
   // Currently, actively-generated enumerators are either basic or variable
   // agnostic.
-  bool isVarAgnostic =
-      isActiveGen
-      && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
+  bool isVarAgnostic = isActiveGen
+                       && options::sygusActiveGenMode()
+                              == options::SygusActiveGenMode::VAR_AGNOSTIC;
   d_enum_var_agnostic[e] = isVarAgnostic;
   if (isVarAgnostic)
   {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 79279eb41..524c440ba 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -16,10 +16,11 @@
 
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "options/theory_options.h"
 #include "options/uf_options.h"
+#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/theory_engine.h"
 
@@ -672,7 +673,8 @@ Node TermDb::evaluateTerm2(TNode n,
             for (unsigned j = 0; j < 2; j++)
             {
               std::pair<bool, Node> et = te->entailmentCheck(
-                  THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate());
+                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
+                  j == 0 ? ret : ret.negate());
               if (et.first)
               {
                 ret = j == 0 ? d_true : d_false;
@@ -905,11 +907,16 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
     return d_has_map.find( n )!=d_has_map.end();
   }else{
     //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
-    if( options::termDbMode()==TERM_DB_ALL ){
+    if (options::termDbMode() == options::TermDbMode::ALL)
+    {
       return true;
-    }else if( options::termDbMode()==TERM_DB_RELEVANT ){
+    }
+    else if (options::termDbMode() == options::TermDbMode::RELEVANT)
+    {
       return d_has_map.find( n )!=d_has_map.end();
-    }else{
+    }
+    else
+    {
       Assert(false);
       return false;
     }
@@ -1061,7 +1068,9 @@ bool TermDb::reset( Theory::Effort effort ){
   }
 
   //compute has map
-  if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){
+  if (options::termDbMode() == options::TermDbMode::RELEVANT
+      || options::lteRestrictInstClosure())
+  {
     d_has_map.clear();
     d_term_elig_eqc.clear();
     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8730e3a97..c7eafc3b8 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -160,7 +160,7 @@ class QuantifiersEnginePrivate
       d_lte_part_inst.reset(new quantifiers::LtePartialInst(qe, c));
       modules.push_back(d_lte_part_inst.get());
     }
-    if (options::quantDynamicSplit() != quantifiers::QUANT_DSPLIT_MODE_NONE)
+    if (options::quantDynamicSplit() != options::QuantDSplitMode::NONE)
     {
       d_qsplit.reset(new quantifiers::QuantDSplit(qe, c));
       modules.push_back(d_qsplit.get());
@@ -273,8 +273,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   // if we require specialized ways of building the model
   if( needsBuilder ){
     Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl;
-    if (options::mbqiMode() == quantifiers::MBQI_FMC
-        || options::mbqiMode() == quantifiers::MBQI_TRUST
+    if (options::mbqiMode() == options::MbqiMode::FMC
+        || options::mbqiMode() == options::MbqiMode::TRUST
         || options::fmfBound())
     {
       Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
@@ -1082,17 +1082,29 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl;
   //determine if we should perform check, based on instWhenMode
   bool performCheck = false;
-  if( options::instWhenMode()==quantifiers::INST_WHEN_FULL ){
+  if (options::instWhenMode() == options::InstWhenMode::FULL)
+  {
     performCheck = ( e >= Theory::EFFORT_FULL );
-  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY ){
+  }
+  else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
+  {
     performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
-  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_LAST_CALL ){
+  }
+  else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
+  {
     performCheck = ( ( e==Theory::EFFORT_FULL && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
-  }else if( options::instWhenMode()==quantifiers::INST_WHEN_FULL_DELAY_LAST_CALL ){
+  }
+  else if (options::instWhenMode()
+           == options::InstWhenMode::FULL_DELAY_LAST_CALL)
+  {
     performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
-  }else if( options::instWhenMode()==quantifiers::INST_WHEN_LAST_CALL ){
+  }
+  else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
+  {
     performCheck = ( e >= Theory::EFFORT_LAST_CALL );
-  }else{
+  }
+  else
+  {
     performCheck = true;
   }
   if( e==Theory::EFFORT_LAST_CALL ){
@@ -1105,10 +1117,15 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   return performCheck;
 }
 
-quantifiers::UserPatMode QuantifiersEngine::getInstUserPatMode() {
-  if( options::userPatternsQuant()==quantifiers::USER_PAT_MODE_INTERLEAVE ){
-    return d_ierCounter%2==0 ? quantifiers::USER_PAT_MODE_USE : quantifiers::USER_PAT_MODE_RESORT;
-  }else{
+options::UserPatMode QuantifiersEngine::getInstUserPatMode()
+{
+  if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
+  {
+    return d_ierCounter % 2 == 0 ? options::UserPatMode::USE
+                                 : options::UserPatMode::RESORT;
+  }
+  else
+  {
     return options::userPatternsQuant();
   }
 }
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index d1d7f1633..380e0896e 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -214,8 +214,9 @@ public:
   /** get needs check */
   bool getInstWhenNeedsCheck( Theory::Effort e );
   /** get user pat mode */
-  quantifiers::UserPatMode getInstUserPatMode();
-public:
+  options::UserPatMode getInstUserPatMode();
+
+ public:
   /** add term to database */
   void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
   /** notification when master equality engine is updated */
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 44d29d819..7a99ed2d9 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -17,10 +17,11 @@
 
 #include "theory/rewriter.h"
 
-#include "theory/theory.h"
+#include "options/theory_options.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/rewriter_tables.h"
+#include "theory/theory.h"
 #include "util/resource_manager.h"
 
 using namespace std;
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index d1ecef831..33a50960c 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -394,7 +394,10 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map<
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       bool processChild = true;
       if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
-        processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1;
+        processChild =
+            options::userPatternsQuant() == options::UserPatMode::IGNORE
+                ? i == 1
+                : i >= 1;
       }
       if( processChild ){
         children.push_back( n[i] );
@@ -650,7 +653,10 @@ Node SortInference::simplifyNode(
     for( size_t i=0; i<n.getNumChildren(); i++ ){
       bool processChild = true;
       if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){
-        processChild = options::userPatternsQuant()==theory::quantifiers::USER_PAT_MODE_IGNORE ? i==1 : i>=1;
+        processChild =
+            options::userPatternsQuant() == options::UserPatMode::IGNORE
+                ? i == 1
+                : i >= 1;
       }
       if( processChild ){
         if( n.getKind()==kind::APPLY_UF ){
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index b13b64f98..e4fe2cf17 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -374,7 +374,7 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
 bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
 {
   // do not compute intersections if the re intersection mode is none
-  if (options::stringRegExpInterMode() == RE_INTER_NONE)
+  if (options::stringRegExpInterMode() == options::RegExpInterMode::NONE)
   {
     return true;
   }
@@ -397,19 +397,21 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
     }
     RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]);
     if (rct == RE_C_VARIABLE
-        || (options::stringRegExpInterMode() == RE_INTER_CONSTANT
+        || (options::stringRegExpInterMode()
+                == options::RegExpInterMode::CONSTANT
             && rct != RE_C_CONRETE_CONSTANT))
     {
       // cannot do intersection on RE with variables, or with re.allchar based
       // on option.
       continue;
     }
-    if (options::stringRegExpInterMode() == RE_INTER_ONE_CONSTANT)
+    if (options::stringRegExpInterMode()
+        == options::RegExpInterMode::ONE_CONSTANT)
     {
       if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT)
       {
         // if both have re.allchar, do not do intersection if the
-        // RE_INTER_ONE_CONSTANT option is set.
+        // options::RegExpInterMode::ONE_CONSTANT option is set.
         continue;
       }
     }
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index b69c99e8c..66ae8d6bc 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -284,7 +284,8 @@ void SolverState::setPendingConflictWhen(Node conf)
 
 Node SolverState::getPendingConflict() const { return d_pendingConflict; }
 
-std::pair<bool, Node> SolverState::entailmentCheck(TheoryOfMode mode, TNode lit)
+std::pair<bool, Node> SolverState::entailmentCheck(options::TheoryOfMode mode,
+                                                   TNode lit)
 {
   return d_valuation.entailmentCheck(mode, lit);
 }
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index a2001bb3b..46d198d36 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -22,6 +22,7 @@
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "options/theory_options.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
 
@@ -171,7 +172,7 @@ class SolverState
    *
    * This calls entailmentCheck on the Valuation object of theory of strings.
    */
-  std::pair<bool, Node> entailmentCheck(TheoryOfMode mode, TNode lit);
+  std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
   /** Separate by length
    *
    * Separate the string representatives in argument n into a partition cols
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index df2364790..7b00ed2e2 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -20,6 +20,7 @@
 
 #include "expr/kind.h"
 #include "options/strings_options.h"
+#include "options/theory_options.h"
 #include "smt/command.h"
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
@@ -3369,7 +3370,7 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
                       Node lt2 = e==0 ? length_term_j : length_term_i;
                       Node ent_lit = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::GT, lt1, lt2 ) );
                       std::pair<bool, Node> et = d_state.entailmentCheck(
-                          THEORY_OF_TYPE_BASED, ent_lit);
+                          options::TheoryOfMode::THEORY_OF_TYPE_BASED, ent_lit);
                       if( et.first ){
                         Trace("strings-entail") << "Strings entailment : " << ent_lit << " is entailed in the current context." << std::endl;
                         Trace("strings-entail") << "  explanation was : " << et.second << std::endl;
@@ -3482,11 +3483,11 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
                                                             int index,
                                                             InferInfo& info)
 {
-  if (options::stringProcessLoopMode() == ProcessLoopMode::ABORT)
+  if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT)
   {
     throw LogicException("Looping word equation encountered.");
   }
-  else if (options::stringProcessLoopMode() == ProcessLoopMode::NONE)
+  else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE)
   {
     d_out->setIncomplete();
     return ProcessLoopResult::SKIPPED;
@@ -3629,11 +3630,13 @@ TheoryStrings::ProcessLoopResult TheoryStrings::processLoop(NormalForm& nfi,
   }
   else
   {
-    if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE_ABORT)
+    if (options::stringProcessLoopMode()
+        == options::ProcessLoopMode::SIMPLE_ABORT)
     {
       throw LogicException("Normal looping word equation encountered.");
     }
-    else if (options::stringProcessLoopMode() == ProcessLoopMode::SIMPLE)
+    else if (options::stringProcessLoopMode()
+             == options::ProcessLoopMode::SIMPLE)
     {
       d_out->setIncomplete();
       return ProcessLoopResult::SKIPPED;
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 719239806..a159787f9 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -16,13 +16,14 @@
 
 #include "theory/theory.h"
 
-#include <vector>
-#include <sstream>
 #include <iostream>
+#include <sstream>
 #include <string>
+#include <vector>
 
 #include "base/check.h"
 #include "expr/node_algorithm.h"
+#include "options/theory_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/ext_theory.h"
 #include "theory/quantifiers_engine.h"
@@ -90,87 +91,128 @@ Theory::~Theory() {
   delete d_extTheory;
 }
 
-TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
+TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
+{
   TheoryId tid = THEORY_BUILTIN;
   switch(mode) {
-  case THEORY_OF_TYPE_BASED:
-    // Constants, variables, 0-ary constructors
-    if (node.isVar()) {
-      if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
-        tid = THEORY_UF;
-      }else{
-        tid = Theory::theoryOf(node.getType());
-      }
-    }else if (node.isConst()) {
-      tid = Theory::theoryOf(node.getType());
-    } else if (node.getKind() == kind::EQUAL) {
-      // Equality is owned by the theory that owns the domain
-      tid = Theory::theoryOf(node[0].getType());
-    } else {
-      // Regular nodes are owned by the kind
-      tid = kindToTheoryId(node.getKind());
-    }
-    break;
-  case THEORY_OF_TERM_BASED:
-    // Variables
-    if (node.isVar()) {
-      if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
-        // We treat the variables as uninterpreted
-        tid = s_uninterpretedSortOwner;
-      } else {
-        if( node.getKind() == kind::BOOLEAN_TERM_VARIABLE ){
-          //Boolean vars go to UF
+    case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
+      // Constants, variables, 0-ary constructors
+      if (node.isVar())
+      {
+        if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+        {
           tid = THEORY_UF;
-        }else{
-          // Except for the Boolean ones
-          tid = THEORY_BOOL;
         }
+        else
+        {
+          tid = Theory::theoryOf(node.getType());
+        }
+      }
+      else if (node.isConst())
+      {
+        tid = Theory::theoryOf(node.getType());
       }
-    } else if (node.isConst()) {
-      // Constants go to the theory of the type
-      tid = Theory::theoryOf(node.getType());
-    } else if (node.getKind() == kind::EQUAL) { // Equality
-      // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
-      if (node[0].getKind() == kind::ITE) {
+      else if (node.getKind() == kind::EQUAL)
+      {
+        // Equality is owned by the theory that owns the domain
         tid = Theory::theoryOf(node[0].getType());
-      } else if (node[1].getKind() == kind::ITE) {
-        tid = Theory::theoryOf(node[1].getType());
-      } else {
-        TNode l = node[0];
-        TNode r = node[1];
-        TypeNode ltype = l.getType();
-        TypeNode rtype = r.getType();
-        if( ltype != rtype ){
-          tid = Theory::theoryOf(l.getType());
-        }else {
-          // If both sides belong to the same theory the choice is easy
-          TheoryId T1 = Theory::theoryOf(l);
-          TheoryId T2 = Theory::theoryOf(r);
-          if (T1 == T2) {
-            tid = T1;
-          } else {
-            TheoryId T3 = Theory::theoryOf(ltype);
-            // This is a case of
-            // * x*y = f(z) -> UF
-            // * x = c      -> UF
-            // * f(x) = read(a, y) -> either UF or ARRAY
-            // at least one of the theories has to be parametric, i.e. theory of the type is different
-            // from the theory of the term
-            if (T1 == T3) {
-              tid = T2;
-            } else if (T2 == T3) {
+      }
+      else
+      {
+        // Regular nodes are owned by the kind
+        tid = kindToTheoryId(node.getKind());
+      }
+      break;
+    case options::TheoryOfMode::THEORY_OF_TERM_BASED:
+      // Variables
+      if (node.isVar())
+      {
+        if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
+        {
+          // We treat the variables as uninterpreted
+          tid = s_uninterpretedSortOwner;
+        }
+        else
+        {
+          if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+          {
+            // Boolean vars go to UF
+            tid = THEORY_UF;
+          }
+          else
+          {
+            // Except for the Boolean ones
+            tid = THEORY_BOOL;
+          }
+        }
+      }
+      else if (node.isConst())
+      {
+        // Constants go to the theory of the type
+        tid = Theory::theoryOf(node.getType());
+      }
+      else if (node.getKind() == kind::EQUAL)
+      {  // Equality
+        // If one of them is an ITE, it's irelevant, since they will get
+        // replaced out anyhow
+        if (node[0].getKind() == kind::ITE)
+        {
+          tid = Theory::theoryOf(node[0].getType());
+        }
+        else if (node[1].getKind() == kind::ITE)
+        {
+          tid = Theory::theoryOf(node[1].getType());
+        }
+        else
+        {
+          TNode l = node[0];
+          TNode r = node[1];
+          TypeNode ltype = l.getType();
+          TypeNode rtype = r.getType();
+          if (ltype != rtype)
+          {
+            tid = Theory::theoryOf(l.getType());
+          }
+          else
+          {
+            // If both sides belong to the same theory the choice is easy
+            TheoryId T1 = Theory::theoryOf(l);
+            TheoryId T2 = Theory::theoryOf(r);
+            if (T1 == T2)
+            {
               tid = T1;
-            } else {
-              // If both are parametric, we take the smaller one (arbitrary)
-              tid = T1 < T2 ? T1 : T2;
+            }
+            else
+            {
+              TheoryId T3 = Theory::theoryOf(ltype);
+              // This is a case of
+              // * x*y = f(z) -> UF
+              // * x = c      -> UF
+              // * f(x) = read(a, y) -> either UF or ARRAY
+              // at least one of the theories has to be parametric, i.e. theory
+              // of the type is different from the theory of the term
+              if (T1 == T3)
+              {
+                tid = T2;
+              }
+              else if (T2 == T3)
+              {
+                tid = T1;
+              }
+              else
+              {
+                // If both are parametric, we take the smaller one (arbitrary)
+                tid = T1 < T2 ? T1 : T2;
+              }
             }
           }
         }
       }
-    } else {
-      // Regular nodes are owned by the kind
-      tid = kindToTheoryId(node.getKind());
-    }
+      else
+      {
+        // Regular nodes are owned by the kind
+        tid = kindToTheoryId(node.getKind());
+      }
     break;
   default:
     Unreachable();
diff --git a/src/theory/theory.h b/src/theory/theory.h
index b133b878e..36db0fda8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -33,7 +33,6 @@
 #include "lib/ffs.h"
 #include "options/options.h"
 #include "options/theory_options.h"
-#include "options/theoryof_mode.h"
 #include "smt/command.h"
 #include "smt/dump.h"
 #include "smt/logic_request.h"
@@ -273,7 +272,7 @@ public:
   /**
    * Returns the ID of the theory responsible for the given node.
    */
-  static TheoryId theoryOf(TheoryOfMode mode, TNode node);
+  static TheoryId theoryOf(options::TheoryOfMode mode, TNode node);
 
   /**
    * Returns the ID of the theory responsible for the given node.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 0a70ddab4..7549bd973 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -29,6 +29,7 @@
 #include "options/options.h"
 #include "options/proof_options.h"
 #include "options/quantifiers_options.h"
+#include "options/theory_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "proof/cnf_proof.h"
 #include "proof/lemma_proof.h"
@@ -2001,7 +2002,7 @@ void TheoryEngine::staticInitializeBVOptions(
     const std::vector<Node>& assertions)
 {
   bool useSlicer = true;
-  if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_ON)
+  if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::ON)
   {
     if (!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified())
       throw ModalException(
@@ -2016,11 +2017,11 @@ void TheoryEngine::staticInitializeBVOptions(
           "Slicer does not currently support model generation. Use "
           "--bv-eq-slicer=off");
   }
-  else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_OFF)
+  else if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::OFF)
   {
     return;
   }
-  else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_AUTO)
+  else if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::AUTO)
   {
     if ((!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified())
         || options::incrementalSolving()
@@ -2242,7 +2243,12 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   }
 }
 
-std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) {
+std::pair<bool, Node> TheoryEngine::entailmentCheck(
+    options::TheoryOfMode mode,
+    TNode lit,
+    const EntailmentCheckParameters* params,
+    EntailmentCheckSideEffects* seffects)
+{
   TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
   if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){
     //Boolean connective, recurse
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index dd34ae16b..5506b0120 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -23,14 +23,15 @@
 #include <memory>
 #include <set>
 #include <unordered_map>
-#include <vector>
 #include <utility>
+#include <vector>
 
 #include "base/check.h"
 #include "context/cdhashset.h"
 #include "expr/node.h"
 #include "options/options.h"
 #include "options/smt_options.h"
+#include "options/theory_options.h"
 #include "prop/prop_engine.h"
 #include "smt/command.h"
 #include "smt_util/lemma_channels.h"
@@ -864,10 +865,13 @@ public:
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */
-  std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
-
-private:
+  std::pair<bool, Node> entailmentCheck(
+      options::TheoryOfMode mode,
+      TNode lit,
+      const theory::EntailmentCheckParameters* params = NULL,
+      theory::EntailmentCheckSideEffects* out = NULL);
 
+ private:
   /** Default visitor for pre-registration */
   PreRegisterVisitor d_preRegistrationVisitor;
 
diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index 26d83334d..01d25860c 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -42,7 +42,7 @@ TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator(
       }
       Unreachable();
       ${mk_type_enumerator_cases}
-#line 44 "${template}"
+#line 46 "${template}"
     default: Unhandled() << "No type enumerator for type `" << type << "'";
   }
   Unreachable();
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 98e330df4..34952084b 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -480,7 +480,7 @@ SortModel::SortModel(Node n,
 {
   d_cardinality_term = n;
 
-  if (options::ufssMode() == UF_SS_FULL)
+  if (options::ufssMode() == options::UfssMode::FULL)
   {
     // Register the strategy with the decision manager of the theory.
     // We are guaranteed that the decision manager is ready since we
@@ -671,7 +671,7 @@ bool SortModel::areDisequal( Node a, Node b ) {
 
 /** check */
 void SortModel::check( Theory::Effort level, OutputChannel* out ){
-  Assert(options::ufssMode() == UF_SS_FULL);
+  Assert(options::ufssMode() == options::UfssMode::FULL);
   if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
     Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type
                    << std::endl;
@@ -1314,7 +1314,7 @@ CardinalityExtension::CardinalityExtension(context::Context* c,
       d_min_pos_tn_master_card(c, -1),
       d_rel_eqc(c)
 {
-  if (options::ufssMode() == UF_SS_FULL && options::ufssFairness())
+  if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
   {
     // Register the strategy with the decision manager of the theory.
     // We are guaranteed that the decision manager is ready since we
@@ -1451,7 +1451,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
 #endif
   bool polarity = n.getKind() != kind::NOT;
   TNode lit = polarity ? n : n[0];
-  if( options::ufssMode()==UF_SS_FULL ){
+  if (options::ufssMode() == options::UfssMode::FULL)
+  {
     if( lit.getKind()==CARDINALITY_CONSTRAINT ){
       TypeNode tn = lit[0].getType();
       Assert(tn.isSort());
@@ -1532,7 +1533,9 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
         }
       }
     }
-  }else{
+  }
+  else
+  {
     if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
       // cardinality constraint from user input, set incomplete   
       Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
@@ -1566,7 +1569,8 @@ bool CardinalityExtension::areDisequal(Node a, Node b)
 void CardinalityExtension::check(Theory::Effort level)
 {
   if( !d_conflict ){
-    if( options::ufssMode()==UF_SS_FULL ){
+    if (options::ufssMode() == options::UfssMode::FULL)
+    {
       Trace("uf-ss-solver")
           << "CardinalityExtension: check " << level << std::endl;
       if (level == Theory::EFFORT_FULL)
@@ -1593,7 +1597,9 @@ void CardinalityExtension::check(Theory::Effort level)
           break;
         }
       }
-    }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){
+    }
+    else if (options::ufssMode() == options::UfssMode::NO_MINIMAL)
+    {
       if( level==Theory::EFFORT_FULL ){
         // split on an equality between two equivalence classes (at most one per type)
         std::map< TypeNode, std::vector< Node > > eqc_list;
@@ -1625,7 +1631,9 @@ void CardinalityExtension::check(Theory::Effort level)
           ++eqcs_i;
         }
       }
-    }else{
+    }
+    else
+    {
       // unhandled uf ss mode
       Assert(false);
     }
@@ -1664,7 +1672,8 @@ CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const
 
 void CardinalityExtension::preRegisterTerm(TNode n)
 {
-  if( options::ufssMode()==UF_SS_FULL ){
+  if (options::ufssMode() == options::UfssMode::FULL)
+  {
     //initialize combined cardinality
     initializeCombinedCardinality();
 
@@ -1776,7 +1785,7 @@ void CardinalityExtension::initializeCombinedCardinality()
 /** check */
 void CardinalityExtension::checkCombinedCardinality()
 {
-  Assert(options::ufssMode() == UF_SS_FULL);
+  Assert(options::ufssMode() == options::UfssMode::FULL);
   if( options::ufssFairness() ){
     Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
     int totalCombinedCard = 0;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 95e3f702b..4d13bf3f2 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -79,7 +79,7 @@ void TheoryUF::finishInit() {
   // finite model finding is enabled, and it is not disabled by
   // options::ufssMode().
   if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind()
-      && options::ufssMode() != UF_SS_NONE)
+      && options::ufssMode() != options::UfssMode::NONE)
   {
     d_thss.reset(new CardinalityExtension(
         getSatContext(), getUserContext(), *d_out, this));
diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index 83a7e3bff..4ad8c8785 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -14,10 +14,12 @@
  ** Implementation of Valuation class.
  **/
 
-#include "expr/node.h"
 #include "theory/valuation.h"
-#include "theory/theory_engine.h"
+
+#include "expr/node.h"
+#include "options/theory_options.h"
 #include "theory/rewriter.h"
+#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace theory {
@@ -123,7 +125,12 @@ unsigned Valuation::getAssertionLevel() const{
   return d_engine->getPropEngine()->getAssertionLevel();
 }
 
-std::pair<bool, Node> Valuation::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params, theory::EntailmentCheckSideEffects* out) {
+std::pair<bool, Node> Valuation::entailmentCheck(
+    options::TheoryOfMode mode,
+    TNode lit,
+    const theory::EntailmentCheckParameters* params,
+    theory::EntailmentCheckSideEffects* out)
+{
   return d_engine->entailmentCheck(mode, lit, params, out);
 }
 
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 89f286a5e..4667db0e9 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -22,7 +22,7 @@
 #define CVC4__THEORY__VALUATION_H
 
 #include "expr/node.h"
-#include "options/theoryof_mode.h"
+#include "options/theory_options.h"
 
 namespace CVC4 {
 
@@ -141,7 +141,11 @@ public:
    * Request an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */
-  std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
+  std::pair<bool, Node> entailmentCheck(
+      options::TheoryOfMode mode,
+      TNode lit,
+      const theory::EntailmentCheckParameters* params = NULL,
+      theory::EntailmentCheckSideEffects* out = NULL);
 
   /** need check ? */
   bool needCheck() const;