diff options
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index efde513a9..f1e178055 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -374,7 +374,7 @@ class TheoryEngine : protected EnvObj * relevance manager failed to compute relevant assertions due to an internal * error. */ - const std::unordered_set<TNode>& getRelevantAssertions(bool& success); + std::unordered_set<TNode> getRelevantAssertions(bool& success); /** * Get difficulty map, which populates dmap, mapping preprocessed assertions @@ -384,6 +384,9 @@ class TheoryEngine : protected EnvObj */ void getDifficultyMap(std::map<Node, Node>& dmap); + /** Get incomplete id, valid immediately after an `unknown` response. */ + theory::IncompleteId getIncompleteId() const; + /** * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). @@ -544,11 +547,6 @@ class TheoryEngine : protected EnvObj 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> d_emptyRelevantSet; /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; |