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.

1 files changed, 7 insertions, 6 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 8b9204a20..d95572820 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -82,23 +82,23 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
 
       if (id == theory::THEORY_BV) {
         auto thBv = static_cast<theory::bv::TheoryBV*>(th);
-        if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
-            && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT)
+        if (options::bitblastMode() == options::BitblastMode::EAGER
+            && options::bvSatSolver() == options::SatSolverMode::CRYPTOMINISAT)
         {
           proof::BitVectorProof* bvp = nullptr;
           switch (options::bvProofFormat())
           {
-            case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT:
+            case options::BvProofFormat::DRAT:
             {
               bvp = new proof::LfscDratBitVectorProof(thBv, this);
               break;
             }
-            case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT:
+            case options::BvProofFormat::LRAT:
             {
               bvp = new proof::LfscLratBitVectorProof(thBv, this);
               break;
             }
-            case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER:
+            case options::BvProofFormat::ER:
             {
               bvp = new proof::LfscErBitVectorProof(thBv, this);
               break;
@@ -585,7 +585,8 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
   //  finalizeBvConflicts(lemmas, os, paren, map);
   ProofManager::getBitVectorProof()->printBBDeclarationAndCnf(os, paren, map);
 
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     Assert(lemmas.size() == 1);
     // nothing more to do (no combination with eager so far)
     return;