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.

5 files changed, 21 insertions, 24 deletions

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 98f57e25f..c60cc8274 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -224,7 +224,7 @@ void BitVectorProof::printOwnedTerm(Expr term,
 void BitVectorProof::printEmptyClauseProof(std::ostream& os,
                                            std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER)
       << "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode";
 }
@@ -644,8 +644,8 @@ void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
   std::vector<Expr>::const_iterator it = d_bbTerms.begin();
   std::vector<Expr>::const_iterator end = d_bbTerms.end();
   for (; it != end; ++it) {
-    if (d_usedBB.find(*it) == d_usedBB.end() &&
-        options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER)
+    if (d_usedBB.find(*it) == d_usedBB.end()
+        && options::bitblastMode() != options::BitblastMode::EAGER)
       continue;
 
     // Is this term has an alias, we inject it through the decl_bblast statement
@@ -668,8 +668,8 @@ void BitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
   ExprToExpr::const_iterator ait = d_bbAtoms.begin();
   ExprToExpr::const_iterator aend = d_bbAtoms.end();
   for (; ait != aend; ++ait) {
-    if (d_usedBB.find(ait->first) == d_usedBB.end() &&
-        options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER)
+    if (d_usedBB.find(ait->first) == d_usedBB.end()
+        && options::bitblastMode() != options::BitblastMode::EAGER)
       continue;
 
     os << "(th_let_pf _ ";
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index bb9213b4b..6b0a57725 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -131,11 +131,8 @@ void ClausalBitVectorProof::optimizeDratProof()
 {
   TimerStat::CodeTimer optimizeDratProofTimer{
       d_dratOptimizationStatistics.d_totalTime};
-  if (options::bvOptimizeSatProof()
-          == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF
-      || options::bvOptimizeSatProof()
-             == theory::bv::BvOptimizeSatProof::
-                    BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+  if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::PROOF
+      || options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA)
   {
     Debug("bv::clausal") << "Optimizing DRAT" << std::endl;
     std::string formulaFilename("cvc4-dimacs-XXXXXX");
@@ -197,8 +194,7 @@ void ClausalBitVectorProof::optimizeDratProof()
           static_cast<int64_t>(d_binaryDratProof.tellp()) - startPos);
     }
 
-    if (options::bvOptimizeSatProof()
-        == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+    if (options::bvOptimizeSatProof() == options::BvOptimizeSatProof::FORMULA)
     {
       std::ifstream optFormulaStream{optFormulaFilename};
       const int64_t startPos = static_cast<int64_t>(optFormulaStream.tellg());
@@ -339,7 +335,7 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
 void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                    std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER)
       << "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode";
 
@@ -366,7 +362,7 @@ void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
 void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                    std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER)
       << "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode";
 
@@ -396,7 +392,7 @@ void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
 void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                  std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER)
       << "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode";
 
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index bbf5b0064..fda3f7424 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -798,7 +798,7 @@ void LFSCProof::toStream(std::ostream& out) const
     CodeTimer finalProofTimer{
         ProofManager::currentPM()->getStats().d_finalProofTime};
     out << ";; Printing final unsat proof \n";
-    if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
+    if (options::bitblastMode() == options::BitblastMode::EAGER
         && ProofManager::getBitVectorProof())
     {
       ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp
index f4ced1748..8d4b56d54 100644
--- a/src/proof/resolution_bitvector_proof.cpp
+++ b/src/proof/resolution_bitvector_proof.cpp
@@ -129,7 +129,7 @@ void ResolutionBitVectorProof::endBVConflict(
 
 void ResolutionBitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts)
 {
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
     Debug("pf::bv") << "Construct full proof." << std::endl;
     d_resolutionProof->constructProof();
@@ -513,7 +513,7 @@ void LfscResolutionBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
 void LfscResolutionBitVectorProof::printEmptyClauseProof(std::ostream& os,
                                                          std::ostream& paren)
 {
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  Assert(options::bitblastMode() == options::BitblastMode::EAGER)
       << "the BV theory should only be proving bottom directly in the eager "
          "bitblasting mode";
   proof::LFSCProofPrinter::printResolutionEmptyClause(
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;