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/theory/bv/theory_bv.cpp | 35 +++++++++++++++++++++--------------
 1 file changed, 21 insertions(+), 14 deletions(-)

(limited to 'src/theory/bv/theory_bv.cpp')

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 23ffabcd1..afd99647b 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -77,7 +77,8 @@ TheoryBV::TheoryBV(context::Context* c,
   setupExtTheory();
   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     d_eagerSolver.reset(new EagerBitblastSolver(c, this));
     return;
   }
@@ -112,7 +113,8 @@ TheoryBV::TheoryBV(context::Context* c,
 TheoryBV::~TheoryBV() {}
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     return;
   }
   if (options::bitvectorEqualitySolver()) {
@@ -237,7 +239,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
   d_calledPreregister = true;
   Debug("bitvector-preregister") << "TheoryBV::preRegister(" << node << ")" << std::endl;
 
-  if (options::bitblastMode() == BITBLAST_MODE_EAGER)
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
   {
     // the aig bit-blaster option is set heuristically
     // if bv abstraction is used
@@ -325,7 +327,8 @@ void TheoryBV::check(Effort e)
   // we may be getting new assertions so the model cache may not be sound
   d_invalidateModelCache.set(true);
   // if we are using the eager solver
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     // this can only happen on an empty benchmark
     if (!d_eagerSolver->isInitialized()) {
       d_eagerSolver->initialize();
@@ -354,7 +357,6 @@ void TheoryBV::check(Effort e)
     return;
   }
 
-
   if (Theory::fullEffort(e)) {
     ++(d_statistics.d_numCallsToCheckFullEffort);
   } else {
@@ -521,7 +523,8 @@ bool TheoryBV::needsCheckLastEffort() {
 bool TheoryBV::collectModelInfo(TheoryModel* m)
 {
   Assert(!inConflict());
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     if (!d_eagerSolver->collectModelInfo(m, true))
     {
       return false;
@@ -547,7 +550,8 @@ Node TheoryBV::getModelValue(TNode var) {
 
 void TheoryBV::propagate(Effort e) {
   Debug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     return;
   }
 
@@ -910,9 +914,9 @@ void TheoryBV::addSharedTerm(TNode t) {
 
 EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
 {
-  if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
     return EQUALITY_UNKNOWN;
-  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_LAZY);
+  Assert(options::bitblastMode() == options::BitblastMode::LAZY);
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
     if (status != EQUALITY_UNKNOWN) {
@@ -975,9 +979,9 @@ void TheoryBV::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
 
 bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
   bool changed = d_abstractionModule->applyAbstraction(assertions, new_assertions);
-  if (changed &&
-      options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
-      options::bitvectorAig()) {
+  if (changed && options::bitblastMode() == options::BitblastMode::EAGER
+      && options::bitvectorAig())
+  {
     // disable AIG mode
     AlwaysAssert(!d_eagerSolver->isInitialized());
     d_eagerSolver->turnOffAig();
@@ -988,9 +992,12 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions, std::vector
 
 void TheoryBV::setProofLog(proof::BitVectorProof* bvp)
 {
-  if( options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER ){
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
     d_eagerSolver->setProofLog(bvp);
-  }else{
+  }
+  else
+  {
     for( unsigned i=0; i< d_subtheories.size(); i++ ){
       d_subtheories[i]->setProofLog( bvp );
     }
-- 
cgit v1.2.3