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.

1 files changed, 16 insertions, 3 deletions

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<TNode, TNodeHashFunction>& getRelevantAssertions(
+      bool& success);
 
  private:
   /**