diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-14 11:12:30 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-14 16:12:30 +0000 |
| commit | 5f6b4f8dd31e21f935c3f4a441af11e18e12d283 (patch) | |
| tree | add52bead6587b5d0e5407f90e1f3056d05a0305 /src/theory/theory_engine.cpp | |
| parent | f3ecc4bfe17776d08efbbb5ed76a5879efa419ca (diff) | |
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.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 12 |
1 files changed, 12 insertions, 0 deletions
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<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()) { |