From e9499c41f405df8b42fd9ae10004b1b91a869106 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 17 Dec 2019 13:43:44 -0800
Subject: 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.
---
 src/preprocessing/passes/bool_to_bv.cpp        | 11 ++++++-----
 src/preprocessing/passes/bv_abstraction.cpp    |  2 +-
 src/preprocessing/passes/quantifier_macros.cpp |  9 ++++++---
 3 files changed, 13 insertions(+), 9 deletions(-)

(limited to 'src/preprocessing')

diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 520e9f2a7..7787d7631 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -72,7 +72,7 @@ bool BoolToBV::needToRebuild(TNode n) const
 
 Node BoolToBV::lowerAssertion(const TNode& a)
 {
-  bool optionITE = options::boolToBitvector() == BOOL_TO_BV_ITE;
+  bool optionITE = options::boolToBitvector() == options::BoolToBVMode::ITE;
   NodeManager* nm = NodeManager::currentNM();
   std::vector<TNode> visit;
   visit.push_back(a);
@@ -166,7 +166,7 @@ void BoolToBV::lowerNode(const TNode& n)
 
   if (!all_bv || (n.getNumChildren() == 0))
   {
-    if ((options::boolToBitvector() == BOOL_TO_BV_ALL)
+    if ((options::boolToBitvector() == options::BoolToBVMode::ALL)
         && n.getType().isBoolean())
     {
       if (k == kind::CONST_BOOLEAN)
@@ -222,7 +222,8 @@ void BoolToBV::lowerNode(const TNode& n)
   }
 
   NodeBuilder<> builder(new_kind);
-  if ((options::boolToBitvector() == BOOL_TO_BV_ALL) && (new_kind != k))
+  if ((options::boolToBitvector() == options::BoolToBVMode::ALL)
+      && (new_kind != k))
   {
     ++(d_statistics.d_numTermsLowered);
   }
@@ -259,7 +260,7 @@ BoolToBV::Statistics::Statistics()
           "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numIteToBvite);
-  if (options::boolToBitvector() == BOOL_TO_BV_ALL)
+  if (options::boolToBitvector() == options::BoolToBVMode::ALL)
   {
     // these statistics wouldn't be correct in the ITE mode,
     // because it might discard rebuilt nodes if it fails to
@@ -272,7 +273,7 @@ BoolToBV::Statistics::Statistics()
 BoolToBV::Statistics::~Statistics()
 {
   smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite);
-  if (options::boolToBitvector() == BOOL_TO_BV_ALL)
+  if (options::boolToBitvector() == options::BoolToBVMode::ALL)
   {
     smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
     smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index 9c0d0ec68..d62c8a97e 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -53,7 +53,7 @@ PreprocessingPassResult BvAbstraction::applyInternal(
   }
   // If we are using the lazy solver and the abstraction applies, then UF
   // symbols were introduced.
-  if (options::bitblastMode() == bv::BITBLAST_MODE_LAZY && changed)
+  if (options::bitblastMode() == options::BitblastMode::LAZY && changed)
   {
     d_preprocContext->widenLogic(theory::THEORY_UF);
   }
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index 1d834ce60..bc2c136e4 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -18,7 +18,6 @@
 
 #include <vector>
 
-#include "options/quantifiers_modes.h"
 #include "options/quantifiers_options.h"
 #include "proof/proof_manager.h"
 #include "smt/smt_engine.h"
@@ -70,7 +69,8 @@ void QuantifierMacros::clearMaps()
 }
 
 bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){
-  unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1;
+  unsigned rmax =
+      options::macrosQuantMode() == options::MacrosQuantMode::ALL ? 2 : 1;
   for( unsigned r=0; r<rmax; r++ ){
     d_ground_macros = (r==0);
     Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl;
@@ -365,7 +365,10 @@ bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Nod
               if( !containsBadOp( n_def, op, opc, visited ) ){
                 Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl;
                 //must be ground UF term if mode is GROUND_UF
-                if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){
+                if (options::macrosQuantMode()
+                        != options::MacrosQuantMode::GROUND_UF
+                    || isGroundUfTerm(f, n_def))
+                {
                   Trace("macros-debug") << "...respects ground-uf constraint." << std::endl;
                   //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where
                   // x1 ... xn are distinct variables
-- 
cgit v1.2.3