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, 20 insertions, 0 deletions

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<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;
@@ -626,6 +631,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().
    */