From: Andrew Reynolds Date: Tue, 23 Nov 2021 23:24:01 +0000 (-0600) Subject: Make difficulty manager only consider lemmas at full effort (#7685) X-Git-Tag: cvc5-1.0.0~779 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4456074f2c9f23373d6ba4f64de2c0e2128d266a;p=cvc5.git Make difficulty manager only consider lemmas at full effort (#7685) Fixes cvc5/cvc5-projects#350 --- diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index a83167591..6b19f2146 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -29,6 +29,7 @@ RelevanceManager::RelevanceManager(context::Context* lemContext, Valuation val) : d_val(val), d_input(lemContext), d_computed(false), + d_inFullEffortCheck(false), d_success(false), d_trackRSetExp(false), d_miniscopeTopLevel(true) @@ -100,11 +101,14 @@ void RelevanceManager::addAssertionsInternal(std::vector& toProcess) } } -void RelevanceManager::resetRound() +void RelevanceManager::beginRound() { d_computed = false; + d_inFullEffortCheck = true; } +void RelevanceManager::endRound() { d_inFullEffortCheck = false; } + void RelevanceManager::computeRelevance() { d_computed = true; @@ -351,7 +355,9 @@ const std::unordered_set& RelevanceManager::getRelevantAssertions( void RelevanceManager::notifyLemma(Node n) { - if (d_dman != nullptr) + // only consider lemmas that were sent at full effort, when we have a + // complete SAT assignment. + if (d_dman != nullptr && d_inFullEffortCheck) { // ensure we know which literals are relevant, and why computeRelevance(); diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index 287694445..7d6434c6b 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -90,10 +90,12 @@ class RelevanceManager /** Singleton version of above */ void notifyPreprocessedAssertion(Node n); /** - * Reset round, called at the beginning of a full effort check in + * Begin round, called at the beginning of a full effort check in * TheoryEngine. */ - void resetRound(); + void beginRound(); + /** End round, called at the end of a full effort check in TheoryEngine. */ + void endRound(); /** * Is lit part of the current relevant selection? This computes the set of * relevant assertions if not already done so. This call is valid during a @@ -165,6 +167,8 @@ class RelevanceManager std::unordered_set d_rset; /** Have we computed the relevant selection this round? */ bool d_computed; + /** Are we in a full effort check? */ + bool d_inFullEffortCheck; /** * Did we succeed in computing the relevant selection? If this is false, there * was a syncronization issue between the input formula and the satisfying diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8622c86aa..ea1209b47 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -391,7 +391,7 @@ void TheoryEngine::check(Theory::Effort effort) { // to indicate that its information must be recomputed. if (d_relManager != nullptr) { - d_relManager->resetRound(); + d_relManager->beginRound(); } d_tc->resetRound(); } @@ -486,10 +486,18 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas"); Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl; - if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) { - // Do post-processing of model from the theories (e.g. used for THEORY_SEP - // to construct heap model) - d_tc->postProcessModel(d_incomplete.get()); + if (Theory::fullEffort(effort)) + { + if (d_relManager != nullptr) + { + d_relManager->endRound(); + } + if (!d_inConflict && !needCheck()) + { + // Do post-processing of model from the theories (e.g. used for + // THEORY_SEP to construct heap model) + d_tc->postProcessModel(d_incomplete.get()); + } } } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => interrupted" << endl;