From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 5 Feb 2021 20:53:47 +0000 (-0600)
Subject: Minor cleaning of quantifiers engine (#5858)
X-Git-Tag: cvc5-1.0.0~2315
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ea30ab14a8a5093e198e853d422dffd13b52275b;p=cvc5.git

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 c7ef88339..a1d3f0ac7 100644
--- 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 b7a1df8a6..d8f94f864 100644
--- 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