diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-03 16:00:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-03 16:00:26 -0500 |
commit | 8828e545cfb838d806a0ad382671a9af131e8431 (patch) | |
tree | a488c085adf0ba36b2d3a0d24b547c1a2eb29926 /src/theory/theory_engine.h | |
parent | 31b3986ea297d54e828cd6c34e3689435ba63d7c (diff) |
Minor cleanup of quantifiers engine (#4994)
Eventually, QuanitifersEngine should not depend on TheoryEngine. This is a first step in this direction. It eliminates some uses of TheoryEngine and eliminates a unnecessary friend relationship between quantifiers::TermDb and TheoryEngine. Further refactoring will be done in future PRs.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 167bd6d75..30b5d9fbb 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -94,10 +94,6 @@ namespace eq { class EqualityEngine; } // namespace eq -namespace quantifiers { -class TermDb; -} - class EntailmentCheckParameters; class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ @@ -115,7 +111,6 @@ class TheoryEngine { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; friend class theory::CombinationEngine; - friend class theory::quantifiers::TermDb; friend class theory::EngineOutputChannel; friend class theory::CombinationEngine; @@ -373,16 +368,12 @@ class TheoryEngine { /** * Get a pointer to the underlying sat context. */ - inline context::Context* getSatContext() const { - return d_context; - } + context::Context* getSatContext() const { return d_context; } /** * Get a pointer to the underlying user context. */ - inline context::Context* getUserContext() const { - return d_userContext; - } + context::UserContext* getUserContext() const { return d_userContext; } /** * Get a pointer to the underlying quantifiers engine. |