Minor cleaning of quantifiers engine (#5858)

This member is currently unused.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index c7ef88339181136df6f33e9e3f086a2f65236340..a1d3f0ac7822a2906f68124442949cc98f44e9c0 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -75,7 +75,6 @@ QuantifiersEngine::QuantifiersEngine(
 
   d_util.push_back(d_instantiate.get());
 
-  d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
   d_hasAddedLemma = false;
   //don't add true lemma
   d_lemmas_produced_c[d_term_util->d_true] = true;
@@ -463,7 +462,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
     {
       QuantifiersModule::QEffort quant_e =
           static_cast<QuantifiersModule::QEffort>(qef);
-      d_curr_effort_level = quant_e;
       // Force the theory engine to build the model if any module requested it.
       if (needsModelE == quant_e)
       {
@@ -581,7 +579,6 @@ void QuantifiersEngine::check( Theory::Effort e ){
         }
       }
     }
-    d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
     Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl;
     // debug print
     if (d_hasAddedLemma)

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index b7a1df8a624e2c82b4c5adef3ebe9976461e2215..d8f94f86440d1d4e876018ff5c7e0a15521060eb 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -201,8 +201,6 @@ public:
  void markRelevant(Node q);
  /** has added lemma */
  bool hasAddedLemma() const;
- /** get current q effort */
- QuantifiersModule::QEffort getCurrentQEffort() { return d_curr_effort_level; }
  /** get number of waiting lemmas */
  unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); }
  /** get needs check */
@@ -350,8 +348,6 @@ public:
    */
   std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules;
   //------------- temporary information during check
-  /** current effort level */
-  QuantifiersModule::QEffort d_curr_effort_level;
   /** has added lemma this round */
   bool d_hasAddedLemma;
   //------------- end temporary information during check