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.

7 files changed, 40 insertions, 27 deletions

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