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.

diff --git a/src/theory/relevance_manager.cpp b/src/theory/relevance_manager.cpp
index f48ef98c6c8e68a406288b4ed8dd4614a443bf98..68ec573c377c6bb0a1eb4118e8e3cae84f116f3d 100644 (file)
--- a/src/theory/relevance_manager.cpp
+++ b/src/theory/relevance_manager.cpp
@@ -85,12 +85,12 @@ void RelevanceManager::addAssertionsInternal(std::vector<Node>& 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<TNode, int, TNodeHashFunction> 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<TNode, TNodeHashFunction>&
+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 83014bcd6497c6a986ce638a3e3507ce8dc66a4d..ac0ad83b5c158f2f330479f1a22942f312cccbfa 100644 (file)
--- 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<TNode, TNodeHashFunction>& getRelevantAssertions(
+      bool& success);
 
  private:
   /**

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 55c782f2f2e6fa7ea429c466ec2996ec92a0ce76..9f0e3eb82925ba04e88baffc5a407a8b08bd42ac 100644 (file)
--- 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<TNode, TNodeHashFunction>&
+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 b43488fa8242f20cc0423571a5ea8c4df31d1541..09d33edc20842528d378b78bee6171ee823bef27 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -157,6 +157,11 @@ class TheoryEngine {
   std::unique_ptr<theory::DecisionManager> d_decManager;
   /** The relevance manager */
   std::unique_ptr<theory::RelevanceManager> d_relManager;
+  /**
+   * An empty set of relevant assertions, which is returned as a dummy value for
+   * getRelevantAssertions when relevance is disabled.
+   */
+  std::unordered_set<TNode, TNodeHashFunction> 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<TNode, TNodeHashFunction>& getRelevantAssertions(
+      bool& success);
+
   /**
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().