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.

2 files changed, 28 insertions, 25 deletions

diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 698d2a776..9e50433ef 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -48,27 +48,27 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-
-SimpSolver::SimpSolver(CVC4::context::Context* c) :
-    Solver(c)
-  , grow               (opt_grow)
-  , clause_lim         (opt_clause_lim)
-  , subsumption_lim    (opt_subsumption_lim)
-  , simp_garbage_frac  (opt_simp_garbage_frac)
-  , use_asymm          (opt_use_asymm)
-  , use_rcheck         (opt_use_rcheck)
-  , use_elim           (opt_use_elim &&
-                        CVC4::options::bitblastMode() == CVC4::theory::bv::BITBLAST_MODE_EAGER &&
-                        !CVC4::options::produceModels())
-  , merges             (0)
-  , asymm_lits         (0)
-  , eliminated_vars    (0)
-  , elimorder          (1)
-  , use_simplification (!PROOF_ON())
-  , occurs             (ClauseDeleted(ca))
-  , elim_heap          (ElimLt(n_occ))
-  , bwdsub_assigns     (0)
-  , n_touched          (0)
+SimpSolver::SimpSolver(CVC4::context::Context* c)
+    : Solver(c),
+      grow(opt_grow),
+      clause_lim(opt_clause_lim),
+      subsumption_lim(opt_subsumption_lim),
+      simp_garbage_frac(opt_simp_garbage_frac),
+      use_asymm(opt_use_asymm),
+      use_rcheck(opt_use_rcheck),
+      use_elim(opt_use_elim
+               && CVC4::options::bitblastMode()
+                      == CVC4::options::BitblastMode::EAGER
+               && !CVC4::options::produceModels()),
+      merges(0),
+      asymm_lits(0),
+      eliminated_vars(0),
+      elimorder(1),
+      use_simplification(!PROOF_ON()),
+      occurs(ClauseDeleted(ca)),
+      elim_heap(ElimLt(n_occ)),
+      bwdsub_assigns(0),
+      n_touched(0)
 {
 
     vec<Lit> dummy(1,lit_Undef);
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 3cdd6b654..80d767b3d 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -106,15 +106,18 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory
 
   d_context = context;
 
-  if( options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ) {
+  if (options::decisionMode() != options::DecisionMode::INTERNAL)
+  {
     Notice() << "minisat: Incremental solving is forced on (to avoid variable elimination)"
              << " unless using internal decision strategy." << std::endl;
   }
 
   // Create the solver
-  d_minisat = new Minisat::SimpSolver(theoryProxy, d_context,
-                                      options::incrementalSolving() ||
-                                      options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL );
+  d_minisat = new Minisat::SimpSolver(
+      theoryProxy,
+      d_context,
+      options::incrementalSolving()
+          || options::decisionMode() != options::DecisionMode::INTERNAL);
 
   d_statistics.init(d_minisat);
 }