From 5f6b4f8dd31e21f935c3f4a441af11e18e12d283 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 14 Apr 2021 11:12:30 -0500 Subject: Add interface for getting relevant assertions (#5131) This adds an interface to TheoryEngine for getting the current set of relevant assertions if it is available. An interface to this can further be added to the API in a future PR. --- src/theory/relevance_manager.cpp | 15 ++++++++++++++- src/theory/relevance_manager.h | 19 ++++++++++++++++--- src/theory/theory_engine.cpp | 12 ++++++++++++ src/theory/theory_engine.h | 20 ++++++++++++++++++++ 4 files changed, 62 insertions(+), 4 deletions(-) (limited to 'src/theory') diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp index f48ef98c6..68ec573c3 100644 --- a/src/theory/relevance_manager.cpp +++ b/src/theory/relevance_manager.cpp @@ -85,12 +85,12 @@ void RelevanceManager::addAssertionsInternal(std::vector& toProcess) void RelevanceManager::resetRound() { d_computed = false; - d_rset.clear(); } void RelevanceManager::computeRelevance() { d_computed = true; + d_rset.clear(); Trace("rel-manager") << "RelevanceManager::computeRelevance..." << std::endl; std::unordered_map cache; for (const Node& node: d_input) @@ -105,6 +105,7 @@ void RelevanceManager::computeRelevance() Trace("rel-manager") << serr.str() << std::endl; Assert(false) << serr.str(); d_success = false; + d_rset.clear(); return; } } @@ -314,5 +315,17 @@ bool RelevanceManager::isRelevant(Node lit) return d_rset.find(lit) != d_rset.end(); } +const std::unordered_set& +RelevanceManager::getRelevantAssertions(bool& success) +{ + if (!d_computed) + { + computeRelevance(); + } + // update success flag + success = d_success; + return d_rset; +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/relevance_manager.h b/src/theory/relevance_manager.h index 83014bcd6..ac0ad83b5 100644 --- a/src/theory/relevance_manager.h +++ b/src/theory/relevance_manager.h @@ -88,11 +88,24 @@ class RelevanceManager */ void resetRound(); /** - * Is lit part of the current relevant selection? This call is valid during - * full effort check in TheoryEngine. This means that theories can query this - * during FULL or LAST_CALL efforts, through the Valuation class. + * 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 + * full effort check in TheoryEngine, or after TheoryEngine has terminated + * with "sat". This means that theories can query this during FULL or + * LAST_CALL efforts, through the Valuation class. */ bool isRelevant(Node lit); + /** + * Get the current relevant selection (see above). This computes this set + * if not already done so. This call is valid during a full effort check in + * TheoryEngine, or after TheoryEngine has terminated with "sat". This method + * sets the flag success to false if we failed to compute relevant + * assertions, which can occur if + * + * The value of this return is only valid if success was not updated to false. + */ + const std::unordered_set& getRelevantAssertions( + bool& success); private: /** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 55c782f2f..9f0e3eb82 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1114,6 +1114,18 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { return d_sharedSolver->getEqualityStatus(a, b); } +const std::unordered_set& +TheoryEngine::getRelevantAssertions(bool& success) +{ + // if we are not in SAT mode, or there is no relevance manager, we fail + if (!d_inSatMode || d_relManager == nullptr) + { + success = false; + return d_emptyRelevantSet; + } + return d_relManager->getRelevantAssertions(success); +} + Node TheoryEngine::getModelValue(TNode var) { if (var.isConst()) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index b43488fa8..09d33edc2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -157,6 +157,11 @@ class TheoryEngine { std::unique_ptr d_decManager; /** The relevance manager */ std::unique_ptr d_relManager; + /** + * An empty set of relevant assertions, which is returned as a dummy value for + * getRelevantAssertions when relevance is disabled. + */ + std::unordered_set d_emptyRelevantSet; /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; @@ -625,6 +630,21 @@ class TheoryEngine { */ Node getModelValue(TNode var); + /** + * Get relevant assertions. This returns a set of assertions that are + * currently asserted to this TheoryEngine that propositionally entail the + * (preprocessed) input formula and all theory lemmas that have been marked + * NEEDS_JUSTIFY. For more details on this, see relevance_manager.h. + * + * This method updates success to false if the set of relevant assertions + * is not available. This may occur if we are not in SAT mode, if the + * relevance manager is disabled (see option::relevanceFilter) or if the + * relevance manager failed to compute relevant assertions due to an internal + * error. + */ + const std::unordered_set& getRelevantAssertions( + bool& success); + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). -- cgit v1.2.3