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.

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.