Delay enumerative instantiation if theory engine does not need check (#3774)

5 files changed, 30 insertions, 8 deletions

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 1e2e34aa2..47e4a9228 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -77,8 +77,11 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
     }
     if (options::fullSaturateQuant() && !doCheck)
     {
-      doCheck = quant_e == QEFFORT_LAST_CALL;
-      fullEffort = !d_quantEngine->hasAddedLemma();
+      if (!d_quantEngine->theoryEngineNeedsCheck())
+      {
+        doCheck = quant_e == QEFFORT_LAST_CALL;
+        fullEffort = true;
+      }
     }
   }
   if (!doCheck)
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 2b621f6dd..c9ed16a5f 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -133,7 +133,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e)
     activeCheckConj = acnext;
     acnext.clear();
   } while (!activeCheckConj.empty()
-           && !d_quantEngine->getTheoryEngine()->needCheck());
+           && !d_quantEngine->theoryEngineNeedsCheck());
   Trace("cegqi-engine")
       << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 524c440ba..b78263f0e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -403,7 +403,7 @@ void TermDb::computeUfTerms( TNode f ) {
           {
             Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
                                    << n << "!!!!" << std::endl;
-            if (!d_quantEngine->getTheoryEngine()->needCheck())
+            if (!d_quantEngine->theoryEngineNeedsCheck())
             {
               Trace("term-db-lemma") << "  all theories passed with no lemmas."
                                      << std::endl;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 80a493496..1db0937ff 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -617,7 +617,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if( !d_lemmas_waiting.empty() ){
         Trace("quant-engine-debug") << "  lemmas waiting = " << d_lemmas_waiting.size() << std::endl;
       }
-      Trace("quant-engine-debug") << "  Theory engine finished : " << !d_te->needCheck() << std::endl;
+      Trace("quant-engine-debug")
+          << "  Theory engine finished : " << !theoryEngineNeedsCheck()
+          << std::endl;
       Trace("quant-engine-debug") << "  Needs model effort : " << needsModelE << std::endl;
     }
     if( Trace.isOn("quant-engine-ee-pre") ){
@@ -1053,6 +1055,14 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 void QuantifiersEngine::markRelevant( Node q ) {
   d_model->markRelevant( q );
 }
+bool QuantifiersEngine::hasAddedLemma() const
+{
+  return !d_lemmas_waiting.empty() || d_hasAddedLemma;
+}
+bool QuantifiersEngine::theoryEngineNeedsCheck() const
+{
+  return d_te->needCheck();
+}
 
 void QuantifiersEngine::setConflict() { 
   d_conflict = true; 
@@ -1069,7 +1079,7 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   }
   else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
   {
-    performCheck = ( e >= Theory::EFFORT_FULL ) && !getTheoryEngine()->needCheck();
+    performCheck = (e >= Theory::EFFORT_FULL) && !theoryEngineNeedsCheck();
   }
   else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
   {
@@ -1078,7 +1088,9 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   else if (options::instWhenMode()
            == options::InstWhenMode::FULL_DELAY_LAST_CALL)
   {
-    performCheck = ( ( e==Theory::EFFORT_FULL && !getTheoryEngine()->needCheck() && d_ierCounter%d_inst_when_phase!=0 ) || e==Theory::EFFORT_LAST_CALL );
+    performCheck = ((e == Theory::EFFORT_FULL && !theoryEngineNeedsCheck()
+                     && d_ierCounter % d_inst_when_phase != 0)
+                    || e == Theory::EFFORT_LAST_CALL);
   }
   else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
   {
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 380e0896e..5172c1554 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -202,7 +202,14 @@ public:
   /** mark relevant quantified formula, this will indicate it should be checked before the others */
   void markRelevant( Node q );
   /** has added lemma */
-  bool hasAddedLemma() { return !d_lemmas_waiting.empty() || d_hasAddedLemma; }
+  bool hasAddedLemma() const;
+  /** theory engine needs check
+   *
+   * This is true if the theory engine has more constraints to process. When
+   * it is false, we are tentatively going to terminate solving with
+   * sat/unknown. For details, see TheoryEngine::needCheck.
+   */
+  bool theoryEngineNeedsCheck() const;
   /** is in conflict */
   bool inConflict() { return d_conflict; }
   /** set conflict */