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, 6 insertions, 10 deletions

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";