diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_enumerative.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 18 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 9 |
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 */ |